Theorem nfcxfr 2889

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

Syntax hints:   = wceq 1540  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878

This theorem is referenced by:  nfrab1  3423  nfrabw  3440  nfrab  3442  nfdifOLD  4089  nfunOLD  4130  nfinOLD  4184  nfsymdif  4216  nfpw  4578  nfpr  4652  nfsn  4667  nfop  4849  nfint  4916  nfiun  4983  nfiin  4984  nfiung  4985  nfiing  4986  nfiu1OLD  4988  nfii1  4989  nfopab1  5172  nfopab2  5173  nfmpt  5200  nfmpt1  5201  nfxp  5664  nfco  5819  nfcnv  5832  nfdm  5904  nfrn  5905  nfres  5941  nfima  6028  nfpred  6267  nfsuc  6394  nfiota1  6454  nffv  6850  fvmptss  6962  fvmptf  6971  fvopab5  6983  ralrnmptw  7048  ralrnmpt  7050  f1ompt  7065  fompt  7072  f1mpt  7218  fliftfun  7269  nfriota1  7333  riotaprop  7353  nfoprab1  7430  nfoprab2  7431  nfoprab3  7432  nfoprab  7433  nfmpo1  7449  nfmpo2  7450  nfmpo  7451  ovmpos  7517  ov2gf  7518  ov3  7532  nfof  7639  nfofr  7640  nftpos  8217  fvmpocurryd  8227  nffrecs  8239  nfwrecs  8270  nfrecs  8320  nfrdg  8359  rdgsucmptf  8373  rdgsucmptnf  8374  frsucmpt  8383  frsucmptn  8384  nfixpw  8866  nfixp  8867  nfixp1  8868  xpcomco  9008  nfsup  9378  nfinf  9410  nfoi  9443  cnfcom3clem  9636  ttrclselem1  9656  ttrclselem2  9657  nfdju  9838  dfac8clem  9963  iunfo  10470  pwfseqlem2  10590  pwfseqlem4a  10592  pwfseqlem4  10593  reclem2pr  10979  nfseq  13954  nfwrd  14486  nfsum1  15633  nfsum  15634  nfcprod1  15851  nfcprod  15852  symgval  19286  ptbasfi  23502  mbfsup  25599  itg1climres  25649  itg2splitlem  25683  itg2split  25684  nfitg1  25709  nfitg  25710  lgamgulm2  26980  lgseisenlem2  27321  nosupbnd2  27662  noinfbnd2  27677  nfseqs  28222  lfgrnloop  29106  numclwlk2lem2f1o  30359  cnlnadjlem5  32051  2ndresdju  32624  nfesum1  34024  nfesum2  34025  ballotlem7  34521  bnj1230  34786  bnj1476  34831  bnj900  34913  bnj958  34924  bnj1000  34925  bnj1014  34945  bnj1123  34970  bnj1307  35007  bnj1321  35011  bnj1384  35016  bnj1398  35018  bnj1408  35020  bnj1444  35027  bnj1445  35028  bnj1446  35029  bnj1447  35030  bnj1448  35031  bnj1449  35032  bnj1466  35037  bnj1467  35038  bnj1518  35048  bnj1519  35049  bnj1520  35050  bnj1525  35053  bnj1523  35055  cvmcov  35244  nfwsuc  35800  nfwlim  35804  nfaltop  35962  currysetlem1  36929  topdifinfindis  37328  rdgssun  37360  exrecfnlem  37361  finxpreclem6  37378  sdclem1  37731  riotasv2s  38945  cdleme26ee  40348  cdlemefs32sn1aw  40402  cdleme43fsv1snlem  40408  cdleme41sn3a  40421  cdleme32d  40432  cdleme32f  40434  cdleme40m  40455  cdleme40n  40456  ltrniotaval  40569  cdlemksv2  40835  cdlemkuv2  40855  cdlemk36  40901  cdlemk38  40903  cdlemkid  40924  cdlemk19x  40931  cdlemk11t  40934  areaquad  43199  nfscott  44222  nfcoll  44239  binomcxplemdvbinom  44336  binomcxplemdvsum  44338  binomcxplemnotnn0  44339  refsum2cnlem1  45025  eliuniincex  45097  disjrnmpt2  45176  rnmptssbi  45248  allbutfi  45383  allbutfiinf  45410  rexanuz2nf  45482  fmuldfeqlem1  45574  fmuldfeq  45575  mullimc  45608  idlimc  45618  limcperiod  45620  neglimc  45639  addlimc  45640  0ellimcdiv  45641  fnlimcnv  45659  fnlimfvre  45666  fnlimfvre2  45669  fnlimf  45670  fnlimabslt  45671  xlimmnfmpt  45835  xlimpnfmpt  45836  cncfmptssg  45863  cncfshift  45866  cncficcgt0  45880  cncfiooicclem1  45885  dvnmul  45935  dvnprodlem1  45938  itgsinexplem1  45946  itgsubsticclem  45967  stoweidlem14  46006  stoweidlem16  46008  stoweidlem18  46010  stoweidlem22  46014  stoweidlem26  46018  stoweidlem27  46019  stoweidlem31  46023  stoweidlem32  46024  stoweidlem34  46026  stoweidlem35  46027  stoweidlem40  46032  stoweidlem41  46033  stoweidlem42  46034  stoweidlem44  46036  stoweidlem45  46037  stoweidlem46  46038  stoweidlem47  46039  stoweidlem48  46040  stoweidlem50  46042  stoweidlem51  46043  stoweidlem52  46044  stoweidlem53  46045  stoweidlem54  46046  stoweidlem57  46049  stoweidlem59  46051  stoweidlem62  46054  wallispilem5  46061  stirlinglem4  46069  stirlinglem5  46070  stirlinglem8  46073  stirlinglem11  46076  stirlinglem12  46077  stirlinglem13  46078  stirlinglem14  46079  stirlinglem15  46080  fourierdlem20  46119  fourierdlem31  46130  fourierdlem68  46166  fourierdlem80  46178  fourierdlem89  46187  fourierdlem91  46189  fourierdlem103  46201  fourierdlem104  46202  fourierdlem112  46210  fourierdlem115  46213  fourierd  46214  fourierclimd  46215  etransclem48  46274  iundjiun  46452  meaiuninc3v  46476  ovnlerp  46554  ovncvrrp  46556  ovnhoilem1  46593  opnvonmbllem1  46624  iunhoiioolem  46667  vonioo  46674  vonicc  46677  pimdecfgtioc  46707  pimincfltioc  46708  pimdecfgtioo  46709  pimincfltioo  46710  issmff  46726  incsmflem  46733  smfpimltxr  46739  smfconst  46741  decsmflem  46758  smfpreimagtf  46760  smflimlem2  46764  smflim  46769  smfpimgtxr  46772  smfresal  46780  smfmullem2  46784  smfmullem4  46786  smfpimbor1lem2  46791  smflim2  46798  smfpimcclem  46799  smflimmpt  46802  smfsup  46806  smfsupmpt  46807  smfsupxr  46808  smfinf  46810  smfinfmpt  46811  smflimsuplem2  46813  smflimsuplem5  46816  smflimsup  46820  smfliminf  46823  smfpimne2  46832  smfdivdmmbl2  46833  fsupdm  46834  fsupdm2  46835  finfdm  46838  finfdm2  46839  nfafv  47131  nfaov  47174  nfafv2  47213  prmdvdsfmtnof1lem1  47579  nfsetrecs  49669