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  28416  numclwlk2lem2f1o  29663  cnlnadjlem5  31355  2ndresdju  31905  nfesum1  33069  nfesum2  33070  ballotlem7  33565  bnj1230  33844  bnj1476  33889  bnj900  33971  bnj958  33982  bnj1000  33983  bnj1014  34003  bnj1123  34028  bnj1307  34065  bnj1321  34069  bnj1384  34074  bnj1398  34076  bnj1408  34078  bnj1444  34085  bnj1445  34086  bnj1446  34087  bnj1447  34088  bnj1448  34089  bnj1449  34090  bnj1466  34095  bnj1467  34096  bnj1518  34106  bnj1519  34107  bnj1520  34108  bnj1525  34111  bnj1523  34113  cvmcov  34285  nfwsuc  34821  nfwlim  34825  nfaltop  34983  currysetlem1  35876  topdifinfindis  36275  rdgssun  36307  exrecfnlem  36308  finxpreclem6  36325  sdclem1  36659  riotasv2s  37876  cdleme26ee  39279  cdlemefs32sn1aw  39333  cdleme43fsv1snlem  39339  cdleme41sn3a  39352  cdleme32d  39363  cdleme32f  39365  cdleme40m  39386  cdleme40n  39387  ltrniotaval  39500  cdlemksv2  39766  cdlemkuv2  39786  cdlemk36  39832  cdlemk38  39834  cdlemkid  39855  cdlemk19x  39862  cdlemk11t  39865  areaquad  42013  nfscott  43046  nfcoll  43063  binomcxplemdvbinom  43160  binomcxplemdvsum  43162  binomcxplemnotnn0  43163  refsum2cnlem1  43769  eliuniincex  43846  disjrnmpt2  43934  fompt  43938  rnmptssbi  44013  allbutfi  44151  allbutfiinf  44178  rexanuz2nf  44251  fmuldfeqlem1  44346  fmuldfeq  44347  mullimc  44380  idlimc  44390  limcperiod  44392  neglimc  44411  addlimc  44412  0ellimcdiv  44413  fnlimcnv  44431  fnlimfvre  44438  fnlimfvre2  44441  fnlimf  44442  fnlimabslt  44443  xlimmnfmpt  44607  xlimpnfmpt  44608  cncfmptssg  44635  cncfshift  44638  cncficcgt0  44652  cncfiooicclem1  44657  dvnmul  44707  dvnprodlem1  44710  itgsinexplem1  44718  itgsubsticclem  44739  stoweidlem14  44778  stoweidlem16  44780  stoweidlem18  44782  stoweidlem22  44786  stoweidlem26  44790  stoweidlem27  44791  stoweidlem31  44795  stoweidlem32  44796  stoweidlem34  44798  stoweidlem35  44799  stoweidlem40  44804  stoweidlem41  44805  stoweidlem42  44806  stoweidlem44  44808  stoweidlem45  44809  stoweidlem46  44810  stoweidlem47  44811  stoweidlem48  44812  stoweidlem50  44814  stoweidlem51  44815  stoweidlem52  44816  stoweidlem53  44817  stoweidlem54  44818  stoweidlem57  44821  stoweidlem59  44823  stoweidlem62  44826  wallispilem5  44833  stirlinglem4  44841  stirlinglem5  44842  stirlinglem8  44845  stirlinglem11  44848  stirlinglem12  44849  stirlinglem13  44850  stirlinglem14  44851  stirlinglem15  44852  fourierdlem20  44891  fourierdlem31  44902  fourierdlem68  44938  fourierdlem80  44950  fourierdlem89  44959  fourierdlem91  44961  fourierdlem103  44973  fourierdlem104  44974  fourierdlem112  44982  fourierdlem115  44985  fourierd  44986  fourierclimd  44987  etransclem48  45046  iundjiun  45224  meaiuninc3v  45248  ovnlerp  45326  ovncvrrp  45328  ovnhoilem1  45365  opnvonmbllem1  45396  iunhoiioolem  45439  vonioo  45446  vonicc  45449  pimdecfgtioc  45479  pimincfltioc  45480  pimdecfgtioo  45481  pimincfltioo  45482  issmff  45498  incsmflem  45505  smfpimltxr  45511  smfconst  45513  decsmflem  45530  smfpreimagtf  45532  smflimlem2  45536  smflim  45541  smfpimgtxr  45544  smfresal  45552  smfmullem2  45556  smfmullem4  45558  smfpimbor1lem2  45563  smflim2  45570  smfpimcclem  45571  smflimmpt  45574  smfsup  45578  smfsupmpt  45579  smfsupxr  45580  smfinf  45582  smfinfmpt  45583  smflimsuplem2  45585  smflimsuplem5  45588  smflimsup  45592  smfliminf  45595  smfpimne2  45604  smfdivdmmbl2  45605  fsupdm  45606  fsupdm2  45607  finfdm  45610  finfdm2  45611  nfafv  45892  nfaov  45935  nfafv2  45974  prmdvdsfmtnof1lem1  46300  nfsetrecs  47779