Theorem nfcxfr 2905

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

Syntax hints:   = wceq 1541  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2814  df-nfc 2889

This theorem is referenced by:  nfrab1  3426  nfrabw  3440  nfrabwOLD  3441  nfrab  3443  nfdif  4085  nfun  4125  nfin  4176  nfsymdif  4206  nfpw  4579  nfpr  4651  nfsn  4668  nfop  4846  nfint  4917  nfiun  4984  nfiin  4985  nfiung  4986  nfiing  4987  nfiu1  4988  nfii1  4989  nfopab1  5175  nfopab2  5176  nfmpt  5212  nfmpt1  5213  nfxp  5666  nfco  5821  nfcnv  5834  nfdm  5906  nfrn  5907  nfres  5939  nfima  6021  nfpred  6258  nfsuc  6389  nfiota1  6450  nffv  6852  fvmptss  6960  fvmptf  6969  fvopab5  6980  ralrnmptw  7043  ralrnmpt  7045  f1ompt  7058  f1mpt  7207  fliftfun  7256  nfriota1  7319  riotaprop  7340  nfoprab1  7417  nfoprab2  7418  nfoprab3  7419  nfoprab  7420  nfmpo1  7436  nfmpo2  7437  nfmpo  7438  ovmpos  7502  ov2gf  7503  ov3  7516  nfof  7622  nfofr  7623  nftpos  8191  fvmpocurryd  8201  nffrecs  8213  nfwrecs  8246  nfwrecsOLD  8247  nfrecs  8320  nfrdg  8359  rdgsucmptf  8373  rdgsucmptnf  8374  frsucmpt  8383  frsucmptn  8384  nfixpw  8853  nfixp  8854  nfixp1  8855  xpcomco  9005  nfsup  9386  nfinf  9417  nfoi  9449  cnfcom3clem  9640  ttrclselem1  9660  ttrclselem2  9661  nfdju  9842  dfac8clem  9967  iunfo  10474  pwfseqlem2  10594  pwfseqlem4a  10596  pwfseqlem4  10597  reclem2pr  10983  nfseq  13915  nfwrd  14430  nfsum1  15573  nfsum  15574  nfsumOLD  15575  nfcprod1  15792  nfcprod  15793  symgval  19148  ptbasfi  22930  mbfsup  25026  itg1climres  25077  itg2splitlem  25111  itg2split  25112  nfitg1  25136  nfitg  25137  lgamgulm2  26383  lgseisenlem2  26722  nosupbnd2  27062  noinfbnd2  27077  lfgrnloop  28074  numclwlk2lem2f1o  29321  cnlnadjlem5  31011  2ndresdju  31563  nfesum1  32630  nfesum2  32631  ballotlem7  33126  bnj1230  33405  bnj1476  33450  bnj900  33532  bnj958  33543  bnj1000  33544  bnj1014  33564  bnj1123  33589  bnj1307  33626  bnj1321  33630  bnj1384  33635  bnj1398  33637  bnj1408  33639  bnj1444  33646  bnj1445  33647  bnj1446  33648  bnj1447  33649  bnj1448  33650  bnj1449  33651  bnj1466  33656  bnj1467  33657  bnj1518  33667  bnj1519  33668  bnj1520  33669  bnj1525  33672  bnj1523  33674  cvmcov  33848  nfwsuc  34384  nfwlim  34388  nfaltop  34556  currysetlem1  35409  topdifinfindis  35808  rdgssun  35840  exrecfnlem  35841  finxpreclem6  35858  sdclem1  36193  riotasv2s  37411  cdleme26ee  38814  cdlemefs32sn1aw  38868  cdleme43fsv1snlem  38874  cdleme41sn3a  38887  cdleme32d  38898  cdleme32f  38900  cdleme40m  38921  cdleme40n  38922  ltrniotaval  39035  cdlemksv2  39301  cdlemkuv2  39321  cdlemk36  39367  cdlemk38  39369  cdlemkid  39390  cdlemk19x  39397  cdlemk11t  39400  areaquad  41528  nfscott  42501  nfcoll  42518  binomcxplemdvbinom  42615  binomcxplemdvsum  42617  binomcxplemnotnn0  42618  refsum2cnlem1  43224  eliuniincex  43301  disjrnmpt2  43383  fompt  43387  rnmptssbi  43465  allbutfi  43604  allbutfiinf  43631  fmuldfeqlem1  43795  fmuldfeq  43796  mullimc  43829  idlimc  43839  limcperiod  43841  neglimc  43860  addlimc  43861  0ellimcdiv  43862  fnlimcnv  43880  fnlimfvre  43887  fnlimfvre2  43890  fnlimf  43891  fnlimabslt  43892  xlimmnfmpt  44056  xlimpnfmpt  44057  cncfmptssg  44084  cncfshift  44087  cncficcgt0  44101  cncfiooicclem1  44106  dvnmul  44156  dvnprodlem1  44159  itgsinexplem1  44167  itgsubsticclem  44188  stoweidlem14  44227  stoweidlem16  44229  stoweidlem18  44231  stoweidlem22  44235  stoweidlem26  44239  stoweidlem27  44240  stoweidlem31  44244  stoweidlem32  44245  stoweidlem34  44247  stoweidlem35  44248  stoweidlem40  44253  stoweidlem41  44254  stoweidlem42  44255  stoweidlem44  44257  stoweidlem45  44258  stoweidlem46  44259  stoweidlem47  44260  stoweidlem48  44261  stoweidlem50  44263  stoweidlem51  44264  stoweidlem52  44265  stoweidlem53  44266  stoweidlem54  44267  stoweidlem57  44270  stoweidlem59  44272  stoweidlem62  44275  wallispilem5  44282  stirlinglem4  44290  stirlinglem5  44291  stirlinglem8  44294  stirlinglem11  44297  stirlinglem12  44298  stirlinglem13  44299  stirlinglem14  44300  stirlinglem15  44301  fourierdlem20  44340  fourierdlem31  44351  fourierdlem68  44387  fourierdlem80  44399  fourierdlem89  44408  fourierdlem91  44410  fourierdlem103  44422  fourierdlem104  44423  fourierdlem112  44431  fourierdlem115  44434  fourierd  44435  fourierclimd  44436  etransclem48  44495  iundjiun  44673  meaiuninc3v  44697  ovnlerp  44775  ovncvrrp  44777  ovnhoilem1  44814  opnvonmbllem1  44845  iunhoiioolem  44888  vonioo  44895  vonicc  44898  pimdecfgtioc  44928  pimincfltioc  44929  pimdecfgtioo  44930  pimincfltioo  44931  issmff  44947  incsmflem  44954  smfpimltxr  44960  smfconst  44962  decsmflem  44979  smfpreimagtf  44981  smflimlem2  44985  smflim  44990  smfpimgtxr  44993  smfresal  45001  smfmullem2  45005  smfmullem4  45007  smfpimbor1lem2  45012  smflim2  45019  smfpimcclem  45020  smflimmpt  45023  smfsup  45027  smfsupmpt  45028  smfsupxr  45029  smfinf  45031  smfinfmpt  45032  smflimsuplem2  45034  smflimsuplem5  45037  smflimsup  45041  smfliminf  45044  smfpimne2  45053  smfdivdmmbl2  45054  fsupdm  45055  fsupdm2  45056  finfdm  45059  finfdm2  45060  nfafv  45340  nfaov  45383  nfafv2  45422  prmdvdsfmtnof1lem1  45748  nfsetrecs  47103