Theorem nfcxfr 2901

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

Syntax hints:   = wceq 1548  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-nf 1792  df-cleq 2733  df-clel 2816  df-nfc 2890

This theorem is referenced by:  nfrab1  3413  nfrabw  3430  nfrab  3431  nfsymdif  4188  nfpw  4551  nfpr  4627  nfsn  4642  nfop  4823  nfint  4890  nfiun  4956  nfiin  4957  nfiung  4958  nfiing  4959  nfii1  4961  nfopab1  5145  nfopab2  5146  nfmpt  5173  nfmpt1  5174  nfxp  5654  nfco  5810  nfcnv  5823  nfdm  5900  nfrn  5901  nfres  5940  nfima  6027  nfpred  6261  nfsuc  6388  nfiota1  6447  nffv  6841  fvmptss  6952  fvmptf  6961  fvopab5  6973  ralrnmptw  7039  ralrnmpt  7041  f1ompt  7056  fompt  7063  f1mpt  7209  fliftfun  7260  nfriota1  7324  riotaprop  7344  nfoprab1  7421  nfoprab2  7422  nfoprab3  7423  nfoprab  7424  nfmpo1  7440  nfmpo2  7441  nfmpo  7442  ovmpos  7508  ov2gf  7509  ov3  7523  nfof  7630  nfofr  7631  nftpos  8205  fvmpocurryd  8215  nffrecs  8227  nfwrecs  8258  nfrecs  8308  nfrdg  8347  rdgsucmptf  8361  rdgsucmptnf  8362  frsucmpt  8371  frsucmptn  8372  nfixpw  8858  nfixp  8859  nfixp1  8860  xpcomco  8999  nfsup  9358  nfinf  9390  nfoi  9423  cnfcom3clem  9621  ttrclselem1  9641  ttrclselem2  9642  nfdju  9826  dfac8clem  9949  iunfo  10456  pwfseqlem2  10577  pwfseqlem4a  10579  pwfseqlem4  10580  reclem2pr  10966  nfseq  13968  nfwrd  14500  nfsum1  15647  nfsum  15648  nfcprod1  15868  nfcprod  15869  symgval  19341  ptbasfi  23568  mbfsup  25653  itg1climres  25703  itg2splitlem  25737  itg2split  25738  nfitg1  25763  nfitg  25764  lgamgulm2  27021  lgseisenlem2  27361  nosupbnd2  27702  noinfbnd2  27717  nfseqs  28301  lfgrnloop  29216  numclwlk2lem2f1o  30471  cnlnadjlem5  32164  2ndresdju  32745  nfesum1  34236  nfesum2  34237  ballotlem7  34732  bnj1230  34999  bnj1476  35044  bnj900  35126  bnj958  35137  bnj1000  35138  bnj1014  35158  bnj1123  35183  bnj1307  35220  bnj1321  35224  bnj1384  35229  bnj1398  35231  bnj1408  35233  bnj1444  35240  bnj1445  35241  bnj1446  35242  bnj1447  35243  bnj1448  35244  bnj1449  35245  bnj1466  35250  bnj1467  35251  bnj1518  35261  bnj1519  35262  bnj1520  35263  bnj1525  35266  bnj1523  35268  cvmcov  35506  nfwsuc  36059  nfwlim  36063  nfaltop  36223  nfttc  36734  currysetlem1  37315  topdifinfindis  37723  rdgssun  37755  exrecfnlem  37756  finxpreclem6  37773  sdclem1  38125  riotasv2s  39465  cdleme26ee  40867  cdlemefs32sn1aw  40921  cdleme43fsv1snlem  40927  cdleme41sn3a  40940  cdleme32d  40951  cdleme32f  40953  cdleme40m  40974  cdleme40n  40975  ltrniotaval  41088  cdlemksv2  41354  cdlemkuv2  41374  cdlemk36  41420  cdlemk38  41422  cdlemkid  41443  cdlemk19x  41450  cdlemk11t  41453  areaquad  43676  nfscott  44698  nfcoll  44715  binomcxplemdvbinom  44812  binomcxplemdvsum  44814  binomcxplemnotnn0  44815  refsum2cnlem1  45500  eliuniincex  45570  disjrnmpt2  45649  rnmptssbi  45718  allbutfi  45851  allbutfiinf  45877  rexanuz2nf  45949  fmuldfeqlem1  46041  fmuldfeq  46042  mullimc  46075  idlimc  46085  limcperiod  46087  neglimc  46104  addlimc  46105  0ellimcdiv  46106  fnlimcnv  46124  fnlimfvre  46131  fnlimfvre2  46134  fnlimf  46135  fnlimabslt  46136  xlimmnfmpt  46300  xlimpnfmpt  46301  cncfmptssg  46328  cncfshift  46331  cncficcgt0  46345  cncfiooicclem1  46350  dvnmul  46400  dvnprodlem1  46403  itgsinexplem1  46411  itgsubsticclem  46432  stoweidlem14  46471  stoweidlem16  46473  stoweidlem18  46475  stoweidlem22  46479  stoweidlem26  46483  stoweidlem27  46484  stoweidlem31  46488  stoweidlem32  46489  stoweidlem34  46491  stoweidlem35  46492  stoweidlem40  46497  stoweidlem41  46498  stoweidlem42  46499  stoweidlem44  46501  stoweidlem45  46502  stoweidlem46  46503  stoweidlem47  46504  stoweidlem48  46505  stoweidlem50  46507  stoweidlem51  46508  stoweidlem52  46509  stoweidlem53  46510  stoweidlem54  46511  stoweidlem57  46514  stoweidlem59  46516  stoweidlem62  46519  wallispilem5  46526  stirlinglem4  46534  stirlinglem5  46535  stirlinglem8  46538  stirlinglem11  46541  stirlinglem12  46542  stirlinglem13  46543  stirlinglem14  46544  stirlinglem15  46545  fourierdlem20  46584  fourierdlem31  46595  fourierdlem68  46631  fourierdlem80  46643  fourierdlem89  46652  fourierdlem91  46654  fourierdlem103  46666  fourierdlem104  46667  fourierdlem112  46675  fourierdlem115  46678  fourierd  46679  fourierclimd  46680  etransclem48  46739  iundjiun  46917  meaiuninc3v  46941  ovnlerp  47019  ovncvrrp  47021  ovnhoilem1  47058  opnvonmbllem1  47089  iunhoiioolem  47132  vonioo  47139  vonicc  47142  pimdecfgtioc  47172  pimincfltioc  47173  pimdecfgtioo  47174  pimincfltioo  47175  issmff  47191  incsmflem  47198  smfpimltxr  47204  smfconst  47206  decsmflem  47223  smfpreimagtf  47225  smflimlem2  47229  smflim  47234  smfpimgtxr  47237  smfresal  47245  smfmullem2  47249  smfmullem4  47251  smfpimbor1lem2  47256  smflim2  47263  smfpimcclem  47264  smflimmpt  47267  smfsup  47271  smfsupmpt  47272  smfsupxr  47273  smfinf  47275  smfinfmpt  47276  smflimsuplem2  47278  smflimsuplem5  47281  smflimsup  47285  smfliminf  47288  smfpimne2  47297  smfdivdmmbl2  47298  fsupdm  47299  fsupdm2  47300  finfdm  47303  finfdm2  47304  nfafv  47613  nfaov  47656  nfafv2  47695  prmdvdsfmtnof1lem1  48076  nfsetrecs  50190