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  9634  ttrclselem1  9654  ttrclselem2  9655  nfdju  9836  dfac8clem  9961  iunfo  10468  pwfseqlem2  10588  pwfseqlem4a  10590  pwfseqlem4  10591  reclem2pr  10977  nfseq  13952  nfwrd  14484  nfsum1  15632  nfsum  15633  nfcprod1  15850  nfcprod  15851  symgval  19285  ptbasfi  23501  mbfsup  25598  itg1climres  25648  itg2splitlem  25682  itg2split  25683  nfitg1  25708  nfitg  25709  lgamgulm2  26979  lgseisenlem2  27320  nosupbnd2  27661  noinfbnd2  27676  nfseqs  28221  lfgrnloop  29105  numclwlk2lem2f1o  30358  cnlnadjlem5  32050  2ndresdju  32623  nfesum1  34023  nfesum2  34024  ballotlem7  34520  bnj1230  34785  bnj1476  34830  bnj900  34912  bnj958  34923  bnj1000  34924  bnj1014  34944  bnj1123  34969  bnj1307  35006  bnj1321  35010  bnj1384  35015  bnj1398  35017  bnj1408  35019  bnj1444  35026  bnj1445  35027  bnj1446  35028  bnj1447  35029  bnj1448  35030  bnj1449  35031  bnj1466  35036  bnj1467  35037  bnj1518  35047  bnj1519  35048  bnj1520  35049  bnj1525  35052  bnj1523  35054  cvmcov  35243  nfwsuc  35799  nfwlim  35803  nfaltop  35961  currysetlem1  36928  topdifinfindis  37327  rdgssun  37359  exrecfnlem  37360  finxpreclem6  37377  sdclem1  37730  riotasv2s  38944  cdleme26ee  40347  cdlemefs32sn1aw  40401  cdleme43fsv1snlem  40407  cdleme41sn3a  40420  cdleme32d  40431  cdleme32f  40433  cdleme40m  40454  cdleme40n  40455  ltrniotaval  40568  cdlemksv2  40834  cdlemkuv2  40854  cdlemk36  40900  cdlemk38  40902  cdlemkid  40923  cdlemk19x  40930  cdlemk11t  40933  areaquad  43198  nfscott  44221  nfcoll  44238  binomcxplemdvbinom  44335  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  refsum2cnlem1  45024  eliuniincex  45096  disjrnmpt2  45175  rnmptssbi  45247  allbutfi  45382  allbutfiinf  45409  rexanuz2nf  45481  fmuldfeqlem1  45573  fmuldfeq  45574  mullimc  45607  idlimc  45617  limcperiod  45619  neglimc  45638  addlimc  45639  0ellimcdiv  45640  fnlimcnv  45658  fnlimfvre  45665  fnlimfvre2  45668  fnlimf  45669  fnlimabslt  45670  xlimmnfmpt  45834  xlimpnfmpt  45835  cncfmptssg  45862  cncfshift  45865  cncficcgt0  45879  cncfiooicclem1  45884  dvnmul  45934  dvnprodlem1  45937  itgsinexplem1  45945  itgsubsticclem  45966  stoweidlem14  46005  stoweidlem16  46007  stoweidlem18  46009  stoweidlem22  46013  stoweidlem26  46017  stoweidlem27  46018  stoweidlem31  46022  stoweidlem32  46023  stoweidlem34  46025  stoweidlem35  46026  stoweidlem40  46031  stoweidlem41  46032  stoweidlem42  46033  stoweidlem44  46035  stoweidlem45  46036  stoweidlem46  46037  stoweidlem47  46038  stoweidlem48  46039  stoweidlem50  46041  stoweidlem51  46042  stoweidlem52  46043  stoweidlem53  46044  stoweidlem54  46045  stoweidlem57  46048  stoweidlem59  46050  stoweidlem62  46053  wallispilem5  46060  stirlinglem4  46068  stirlinglem5  46069  stirlinglem8  46072  stirlinglem11  46075  stirlinglem12  46076  stirlinglem13  46077  stirlinglem14  46078  stirlinglem15  46079  fourierdlem20  46118  fourierdlem31  46129  fourierdlem68  46165  fourierdlem80  46177  fourierdlem89  46186  fourierdlem91  46188  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem115  46212  fourierd  46213  fourierclimd  46214  etransclem48  46273  iundjiun  46451  meaiuninc3v  46475  ovnlerp  46553  ovncvrrp  46555  ovnhoilem1  46592  opnvonmbllem1  46623  iunhoiioolem  46666  vonioo  46673  vonicc  46676  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  issmff  46725  incsmflem  46732  smfpimltxr  46738  smfconst  46740  decsmflem  46757  smfpreimagtf  46759  smflimlem2  46763  smflim  46768  smfpimgtxr  46771  smfresal  46779  smfmullem2  46783  smfmullem4  46785  smfpimbor1lem2  46790  smflim2  46797  smfpimcclem  46798  smflimmpt  46801  smfsup  46805  smfsupmpt  46806  smfsupxr  46807  smfinf  46809  smfinfmpt  46810  smflimsuplem2  46812  smflimsuplem5  46815  smflimsup  46819  smfliminf  46822  smfpimne2  46831  smfdivdmmbl2  46832  fsupdm  46833  fsupdm2  46834  finfdm  46837  finfdm2  46838  nfafv  47130  nfaov  47173  nfafv2  47212  prmdvdsfmtnof1lem1  47578  nfsetrecs  49668