Theorem nfcxfr 2924

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 2923	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 234	1 ⊢ Ⅎ𝑥𝐴

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-cleq 2755  df-clel 2839  df-nfc 2913

This theorem is used by:  nfrab1  3435  nfrabw  3451  nfrab  3452  nfsymdif  4205  nfpw  4580  nfpr  4653  nfsn  4668  nfop  4852  nfint  4920  nfiun  4985  nfiin  4986  nfiung  4987  nfiing  4988  nfii1  4990  nfopab1  5178  nfopab2  5179  nfmpt  5206  nfmpt1  5207  nfxp  5688  nfco  5848  nfcnv  5862  nfdm  5939  nfrn  5940  nfres  5982  nfima  6075  nfpred  6324  nfsuc  6452  nfiota1  6511  nffv  6915  fvmptss  7026  fvmptf  7035  fvopab5  7047  ralrnmptw  7115  ralrnmpt  7117  f1ompt  7132  fompt  7139  f1mpt  7285  fliftfun  7340  nfriota1  7404  riotaprop  7424  nfoprab1  7501  nfoprab2  7502  nfoprab3  7503  nfoprab  7504  nfmpo1  7520  nfmpo2  7521  nfmpo  7522  ovmpos  7589  ov2gf  7590  ov3  7604  nfof  7720  nfofr  7721  nftpos  8303  fvmpocurryd  8313  nffrecs  8326  nfwrecs  8357  nfrecs  8407  nfrdg  8447  rdgsucmptf  8461  rdgsucmptnf  8462  frsucmpt  8471  frsucmptn  8472  nfixpw  8969  nfixp  8970  nfixp1  8971  xpcomco  9111  nfsup  9467  nfinf  9499  nfoi  9532  cnfcom3clem  9730  ttrclselem1  9750  ttrclselem2  9751  nfscott  9956  nfdju  10012  dfac8clem  10135  iunfo  10647  pwfseqlem2  10768  pwfseqlem4a  10770  pwfseqlem4  10771  reclem2pr  11157  nfseq  14178  nfwrd  14712  nfsum1  15883  nfsum  15884  nfcprod1  16103  nfcprod  16104  symgval  19612  ptbasfi  23927  mbfsup  26012  itg1climres  26062  itg2splitlem  26096  itg2split  26097  nfitg1  26121  nfitg  26122  lgamgulm2  27390  lgseisenlem2  27730  nosupbnd2  28100  noinfbnd2  28115  nfseqs  28700  lfgrnloop  29730  numclwlk2lem2f1o  31007  cnlnadjlem5  32700  2ndresdju  33312  nfesum1  34739  nfesum2  34740  ballotlem7  35235  bnj1230  35499  bnj1476  35544  bnj900  35626  bnj958  35637  bnj1000  35638  bnj1014  35658  bnj1123  35683  bnj1307  35720  bnj1321  35724  bnj1384  35729  bnj1398  35731  bnj1408  35733  bnj1444  35740  bnj1445  35741  bnj1446  35742  bnj1447  35743  bnj1448  35744  bnj1449  35745  bnj1466  35750  bnj1467  35751  bnj1518  35761  bnj1519  35762  bnj1520  35763  bnj1525  35766  bnj1523  35768  rankse  35822  onprcf1acwevdlem2  36045  srepdflem1  36084  srepdflem2  36085  cvmcov  36194  nfwsuc  36757  nfwlim  36761  nfaltop  36922  nfttc  37456  currysetlem1  38037  topdifinfindis  38460  rdgssun  38492  exrecfnlem  38493  finxpreclem6  38510  sdclem1  38868  riotasv2s  40206  cdleme26ee  41608  cdlemefs32sn1aw  41662  cdleme43fsv1snlem  41668  cdleme41sn3a  41681  cdleme32d  41692  cdleme32f  41694  cdleme40m  41715  cdleme40n  41716  ltrniotaval  41829  cdlemksv2  42095  cdlemkuv2  42115  cdlemk36  42161  cdlemk38  42163  cdlemkid  42184  cdlemk19x  42191  cdlemk11t  42194  areaquad  44408  nfcoll  45430  binomcxplemdvbinom  45527  binomcxplemdvsum  45529  binomcxplemnotnn0  45530  refsum2cnlem1  46257  eliuniincex  46327  disjrnmpt2  46406  rnmptssbi  46475  allbutfi  46607  allbutfiinf  46633  rexanuz2nf  46705  fmuldfeqlem1  46797  fmuldfeq  46798  mullimc  46831  idlimc  46841  limcperiod  46843  neglimc  46860  addlimc  46861  0ellimcdiv  46862  fnlimcnv  46880  fnlimfvre  46887  fnlimfvre2  46890  fnlimf  46891  fnlimabslt  46892  xlimmnfmpt  47056  xlimpnfmpt  47057  cncfmptssg  47084  cncfshift  47087  cncficcgt0  47101  cncfiooicclem1  47106  dvnmul  47156  dvnprodlem1  47159  itgsinexplem1  47167  itgsubsticclem  47188  stoweidlem14  47227  stoweidlem16  47229  stoweidlem18  47231  stoweidlem22  47235  stoweidlem26  47239  stoweidlem27  47240  stoweidlem31  47244  stoweidlem32  47245  stoweidlem34  47247  stoweidlem35  47248  stoweidlem40  47253  stoweidlem41  47254  stoweidlem42  47255  stoweidlem44  47257  stoweidlem45  47258  stoweidlem46  47259  stoweidlem47  47260  stoweidlem48  47261  stoweidlem50  47263  stoweidlem51  47264  stoweidlem52  47265  stoweidlem53  47266  stoweidlem54  47267  stoweidlem57  47270  stoweidlem59  47272  stoweidlem62  47275  wallispilem5  47282  stirlinglem4  47290  stirlinglem5  47291  stirlinglem8  47294  stirlinglem11  47297  stirlinglem12  47298  stirlinglem13  47299  stirlinglem14  47300  stirlinglem15  47301  fourierdlem20  47340  fourierdlem31  47351  fourierdlem68  47387  fourierdlem80  47399  fourierdlem89  47408  fourierdlem91  47410  fourierdlem103  47422  fourierdlem104  47423  fourierdlem112  47431  fourierdlem115  47434  fourierd  47435  fourierclimd  47436  etransclem48  47495  iundjiun  47673  meaiuninc3v  47697  ovnlerp  47775  ovncvrrp  47777  ovnhoilem1  47814  opnvonmbllem1  47845  iunhoiioolem  47888  vonioo  47895  vonicc  47898  pimdecfgtioc  47928  pimincfltioc  47929  pimdecfgtioo  47930  pimincfltioo  47931  issmff  47947  incsmflem  47954  smfpimltxr  47960  smfconst  47962  decsmflem  47979  smfpreimagtf  47981  smflimlem2  47985  smflim  47990  smfpimgtxr  47993  smfresal  48001  smfmullem2  48005  smfmullem4  48007  smfpimbor1lem2  48012  smflim2  48019  smfpimcclem  48020  smflimmpt  48023  smfsup  48027  smfsupmpt  48028  smfsupxr  48029  smfinf  48031  smfinfmpt  48032  smflimsuplem2  48034  smflimsuplem5  48037  smflimsup  48041  smfliminf  48044  smfpimne2  48053  smfdivdmmbl2  48054  fsupdm  48055  fsupdm2  48056  finfdm  48059  finfdm2  48060  nfafv  48409  nfaov  48452  nfafv2  48491  prmdvdsfmtnof1lem1  48872  nfsetrecs  51067