Theorem nfcxfr 2903

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfcxfr.1	⊢ 𝐴 = 𝐵
nfcxfr.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcxfr	⊢ Ⅎ𝑥𝐴

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 ⊢ Ⅎ𝑥𝐵
2		nfcxfr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2902	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 231	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1540  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892

This theorem is referenced by:  nfrab1  3457  nfrabw  3475  nfrabwOLD  3476  nfrab  3478  nfdifOLD  4130  nfunOLD  4171  nfinOLD  4225  nfsymdif  4257  nfpw  4619  nfpr  4692  nfsn  4707  nfop  4889  nfint  4956  nfiun  5023  nfiin  5024  nfiung  5025  nfiing  5026  nfiu1OLD  5028  nfii1  5029  nfopab1  5213  nfopab2  5214  nfmpt  5249  nfmpt1  5250  nfxp  5718  nfco  5876  nfcnv  5889  nfdm  5962  nfrn  5963  nfres  5999  nfima  6086  nfpred  6326  nfsuc  6456  nfiota1  6516  nffv  6916  fvmptss  7028  fvmptf  7037  fvopab5  7049  ralrnmptw  7114  ralrnmpt  7116  f1ompt  7131  fompt  7138  f1mpt  7281  fliftfun  7332  nfriota1  7395  riotaprop  7415  nfoprab1  7494  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  nfmpo1  7513  nfmpo2  7514  nfmpo  7515  ovmpos  7581  ov2gf  7582  ov3  7596  nfof  7703  nfofr  7704  nftpos  8286  fvmpocurryd  8296  nffrecs  8308  nfwrecs  8341  nfwrecsOLD  8342  nfrecs  8415  nfrdg  8454  rdgsucmptf  8468  rdgsucmptnf  8469  frsucmpt  8478  frsucmptn  8479  nfixpw  8956  nfixp  8957  nfixp1  8958  xpcomco  9102  nfsup  9491  nfinf  9522  nfoi  9554  cnfcom3clem  9745  ttrclselem1  9765  ttrclselem2  9766  nfdju  9947  dfac8clem  10072  iunfo  10579  pwfseqlem2  10699  pwfseqlem4a  10701  pwfseqlem4  10702  reclem2pr  11088  nfseq  14052  nfwrd  14581  nfsum1  15726  nfsum  15727  nfcprod1  15944  nfcprod  15945  symgval  19388  ptbasfi  23589  mbfsup  25699  itg1climres  25749  itg2splitlem  25783  itg2split  25784  nfitg1  25809  nfitg  25810  lgamgulm2  27079  lgseisenlem2  27420  nosupbnd2  27761  noinfbnd2  27776  nfseqs  28293  lfgrnloop  29142  numclwlk2lem2f1o  30398  cnlnadjlem5  32090  2ndresdju  32659  nfesum1  34041  nfesum2  34042  ballotlem7  34538  bnj1230  34816  bnj1476  34861  bnj900  34943  bnj958  34954  bnj1000  34955  bnj1014  34975  bnj1123  35000  bnj1307  35037  bnj1321  35041  bnj1384  35046  bnj1398  35048  bnj1408  35050  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1447  35060  bnj1448  35061  bnj1449  35062  bnj1466  35067  bnj1467  35068  bnj1518  35078  bnj1519  35079  bnj1520  35080  bnj1525  35083  bnj1523  35085  cvmcov  35268  nfwsuc  35819  nfwlim  35823  nfaltop  35981  currysetlem1  36948  topdifinfindis  37347  rdgssun  37379  exrecfnlem  37380  finxpreclem6  37397  sdclem1  37750  riotasv2s  38959  cdleme26ee  40362  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32d  40446  cdleme32f  40448  cdleme40m  40469  cdleme40n  40470  ltrniotaval  40583  cdlemksv2  40849  cdlemkuv2  40869  cdlemk36  40915  cdlemk38  40917  cdlemkid  40938  cdlemk19x  40945  cdlemk11t  40948  areaquad  43228  nfscott  44258  nfcoll  44275  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  refsum2cnlem1  45042  eliuniincex  45114  disjrnmpt2  45193  rnmptssbi  45267  allbutfi  45404  allbutfiinf  45431  rexanuz2nf  45503  fmuldfeqlem1  45597  fmuldfeq  45598  mullimc  45631  idlimc  45641  limcperiod  45643  neglimc  45662  addlimc  45663  0ellimcdiv  45664  fnlimcnv  45682  fnlimfvre  45689  fnlimfvre2  45692  fnlimf  45693  fnlimabslt  45694  xlimmnfmpt  45858  xlimpnfmpt  45859  cncfmptssg  45886  cncfshift  45889  cncficcgt0  45903  cncfiooicclem1  45908  dvnmul  45958  dvnprodlem1  45961  itgsinexplem1  45969  itgsubsticclem  45990  stoweidlem14  46029  stoweidlem16  46031  stoweidlem18  46033  stoweidlem22  46037  stoweidlem26  46041  stoweidlem27  46042  stoweidlem31  46046  stoweidlem32  46047  stoweidlem34  46049  stoweidlem35  46050  stoweidlem40  46055  stoweidlem41  46056  stoweidlem42  46057  stoweidlem44  46059  stoweidlem45  46060  stoweidlem46  46061  stoweidlem47  46062  stoweidlem48  46063  stoweidlem50  46065  stoweidlem51  46066  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  stoweidlem57  46072  stoweidlem59  46074  stoweidlem62  46077  wallispilem5  46084  stirlinglem4  46092  stirlinglem5  46093  stirlinglem8  46096  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  fourierdlem20  46142  fourierdlem31  46153  fourierdlem68  46189  fourierdlem80  46201  fourierdlem89  46210  fourierdlem91  46212  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem115  46236  fourierd  46237  fourierclimd  46238  etransclem48  46297  iundjiun  46475  meaiuninc3v  46499  ovnlerp  46577  ovncvrrp  46579  ovnhoilem1  46616  opnvonmbllem1  46647  iunhoiioolem  46690  vonioo  46697  vonicc  46700  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  issmff  46749  incsmflem  46756  smfpimltxr  46762  smfconst  46764  decsmflem  46781  smfpreimagtf  46783  smflimlem2  46787  smflim  46792  smfpimgtxr  46795  smfresal  46803  smfmullem2  46807  smfmullem4  46809  smfpimbor1lem2  46814  smflim2  46821  smfpimcclem  46822  smflimmpt  46825  smfsup  46829  smfsupmpt  46830  smfsupxr  46831  smfinf  46833  smfinfmpt  46834  smflimsuplem2  46836  smflimsuplem5  46839  smflimsup  46843  smfliminf  46846  smfpimne2  46855  smfdivdmmbl2  46856  fsupdm  46857  fsupdm2  46858  finfdm  46861  finfdm2  46862  nfafv  47148  nfaov  47191  nfafv2  47230  prmdvdsfmtnof1lem1  47571  nfsetrecs  49205