Theorem nfcxfr 2902

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

Syntax hints:   = wceq 1542  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886

This theorem is referenced by:  nfrab1  3452  nfrabw  3469  nfrabwOLD  3470  nfrab  3473  nfdif  4126  nfun  4166  nfin  4217  nfsymdif  4247  nfpw  4622  nfpr  4695  nfsn  4712  nfop  4890  nfint  4961  nfiun  5028  nfiin  5029  nfiung  5030  nfiing  5031  nfiu1  5032  nfii1  5033  nfopab1  5219  nfopab2  5220  nfmpt  5256  nfmpt1  5257  nfxp  5710  nfco  5866  nfcnv  5879  nfdm  5951  nfrn  5952  nfres  5984  nfima  6068  nfpred  6306  nfsuc  6437  nfiota1  6498  nffv  6902  fvmptss  7011  fvmptf  7020  fvopab5  7031  ralrnmptw  7096  ralrnmpt  7098  f1ompt  7111  f1mpt  7260  fliftfun  7309  nfriota1  7372  riotaprop  7393  nfoprab1  7470  nfoprab2  7471  nfoprab3  7472  nfoprab  7473  nfmpo1  7489  nfmpo2  7490  nfmpo  7491  ovmpos  7556  ov2gf  7557  ov3  7570  nfof  7676  nfofr  7677  nftpos  8246  fvmpocurryd  8256  nffrecs  8268  nfwrecs  8301  nfwrecsOLD  8302  nfrecs  8375  nfrdg  8414  rdgsucmptf  8428  rdgsucmptnf  8429  frsucmpt  8438  frsucmptn  8439  nfixpw  8910  nfixp  8911  nfixp1  8912  xpcomco  9062  nfsup  9446  nfinf  9477  nfoi  9509  cnfcom3clem  9700  ttrclselem1  9720  ttrclselem2  9721  nfdju  9902  dfac8clem  10027  iunfo  10534  pwfseqlem2  10654  pwfseqlem4a  10656  pwfseqlem4  10657  reclem2pr  11043  nfseq  13976  nfwrd  14493  nfsum1  15636  nfsum  15637  nfcprod1  15854  nfcprod  15855  symgval  19236  ptbasfi  23085  mbfsup  25181  itg1climres  25232  itg2splitlem  25266  itg2split  25267  nfitg1  25291  nfitg  25292  lgamgulm2  26540  lgseisenlem2  26879  nosupbnd2  27219  noinfbnd2  27234  lfgrnloop  28385  numclwlk2lem2f1o  29632  cnlnadjlem5  31324  2ndresdju  31874  nfesum1  33038  nfesum2  33039  ballotlem7  33534  bnj1230  33813  bnj1476  33858  bnj900  33940  bnj958  33951  bnj1000  33952  bnj1014  33972  bnj1123  33997  bnj1307  34034  bnj1321  34038  bnj1384  34043  bnj1398  34045  bnj1408  34047  bnj1444  34054  bnj1445  34055  bnj1446  34056  bnj1447  34057  bnj1448  34058  bnj1449  34059  bnj1466  34064  bnj1467  34065  bnj1518  34075  bnj1519  34076  bnj1520  34077  bnj1525  34080  bnj1523  34082  cvmcov  34254  nfwsuc  34790  nfwlim  34794  nfaltop  34952  currysetlem1  35828  topdifinfindis  36227  rdgssun  36259  exrecfnlem  36260  finxpreclem6  36277  sdclem1  36611  riotasv2s  37828  cdleme26ee  39231  cdlemefs32sn1aw  39285  cdleme43fsv1snlem  39291  cdleme41sn3a  39304  cdleme32d  39315  cdleme32f  39317  cdleme40m  39338  cdleme40n  39339  ltrniotaval  39452  cdlemksv2  39718  cdlemkuv2  39738  cdlemk36  39784  cdlemk38  39786  cdlemkid  39807  cdlemk19x  39814  cdlemk11t  39817  areaquad  41965  nfscott  42998  nfcoll  43015  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  refsum2cnlem1  43721  eliuniincex  43798  disjrnmpt2  43886  fompt  43890  rnmptssbi  43965  allbutfi  44103  allbutfiinf  44130  rexanuz2nf  44203  fmuldfeqlem1  44298  fmuldfeq  44299  mullimc  44332  idlimc  44342  limcperiod  44344  neglimc  44363  addlimc  44364  0ellimcdiv  44365  fnlimcnv  44383  fnlimfvre  44390  fnlimfvre2  44393  fnlimf  44394  fnlimabslt  44395  xlimmnfmpt  44559  xlimpnfmpt  44560  cncfmptssg  44587  cncfshift  44590  cncficcgt0  44604  cncfiooicclem1  44609  dvnmul  44659  dvnprodlem1  44662  itgsinexplem1  44670  itgsubsticclem  44691  stoweidlem14  44730  stoweidlem16  44732  stoweidlem18  44734  stoweidlem22  44738  stoweidlem26  44742  stoweidlem27  44743  stoweidlem31  44747  stoweidlem32  44748  stoweidlem34  44750  stoweidlem35  44751  stoweidlem40  44756  stoweidlem41  44757  stoweidlem42  44758  stoweidlem44  44760  stoweidlem45  44761  stoweidlem46  44762  stoweidlem47  44763  stoweidlem48  44764  stoweidlem50  44766  stoweidlem51  44767  stoweidlem52  44768  stoweidlem53  44769  stoweidlem54  44770  stoweidlem57  44773  stoweidlem59  44775  stoweidlem62  44778  wallispilem5  44785  stirlinglem4  44793  stirlinglem5  44794  stirlinglem8  44797  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  fourierdlem20  44843  fourierdlem31  44854  fourierdlem68  44890  fourierdlem80  44902  fourierdlem89  44911  fourierdlem91  44913  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  fourierdlem115  44937  fourierd  44938  fourierclimd  44939  etransclem48  44998  iundjiun  45176  meaiuninc3v  45200  ovnlerp  45278  ovncvrrp  45280  ovnhoilem1  45317  opnvonmbllem1  45348  iunhoiioolem  45391  vonioo  45398  vonicc  45401  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  issmff  45450  incsmflem  45457  smfpimltxr  45463  smfconst  45465  decsmflem  45482  smfpreimagtf  45484  smflimlem2  45488  smflim  45493  smfpimgtxr  45496  smfresal  45504  smfmullem2  45508  smfmullem4  45510  smfpimbor1lem2  45515  smflim2  45522  smfpimcclem  45523  smflimmpt  45526  smfsup  45530  smfsupmpt  45531  smfsupxr  45532  smfinf  45534  smfinfmpt  45535  smflimsuplem2  45537  smflimsuplem5  45540  smflimsup  45544  smfliminf  45547  smfpimne2  45556  smfdivdmmbl2  45557  fsupdm  45558  fsupdm2  45559  finfdm  45562  finfdm2  45563  nfafv  45844  nfaov  45887  nfafv2  45926  prmdvdsfmtnof1lem1  46252  nfsetrecs  47731