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  3415  nfrabw  3432  nfrab  3434  nfdifOLD  4081  nfunOLD  4122  nfinOLD  4176  nfsymdif  4208  nfpw  4570  nfpr  4644  nfsn  4659  nfop  4840  nfint  4906  nfiun  4973  nfiin  4974  nfiung  4975  nfiing  4976  nfiu1OLD  4978  nfii1  4979  nfopab1  5162  nfopab2  5163  nfmpt  5190  nfmpt1  5191  nfxp  5652  nfco  5808  nfcnv  5821  nfdm  5893  nfrn  5894  nfres  5932  nfima  6019  nfpred  6254  nfsuc  6381  nfiota1  6440  nffv  6832  fvmptss  6942  fvmptf  6951  fvopab5  6963  ralrnmptw  7028  ralrnmpt  7030  f1ompt  7045  fompt  7052  f1mpt  7198  fliftfun  7249  nfriota1  7313  riotaprop  7333  nfoprab1  7410  nfoprab2  7411  nfoprab3  7412  nfoprab  7413  nfmpo1  7429  nfmpo2  7430  nfmpo  7431  ovmpos  7497  ov2gf  7498  ov3  7512  nfof  7619  nfofr  7620  nftpos  8194  fvmpocurryd  8204  nffrecs  8216  nfwrecs  8247  nfrecs  8297  nfrdg  8336  rdgsucmptf  8350  rdgsucmptnf  8351  frsucmpt  8360  frsucmptn  8361  nfixpw  8843  nfixp  8844  nfixp1  8845  xpcomco  8984  nfsup  9341  nfinf  9373  nfoi  9406  cnfcom3clem  9601  ttrclselem1  9621  ttrclselem2  9622  nfdju  9803  dfac8clem  9926  iunfo  10433  pwfseqlem2  10553  pwfseqlem4a  10555  pwfseqlem4  10556  reclem2pr  10942  nfseq  13918  nfwrd  14450  nfsum1  15597  nfsum  15598  nfcprod1  15815  nfcprod  15816  symgval  19250  ptbasfi  23466  mbfsup  25563  itg1climres  25613  itg2splitlem  25647  itg2split  25648  nfitg1  25673  nfitg  25674  lgamgulm2  26944  lgseisenlem2  27285  nosupbnd2  27626  noinfbnd2  27641  nfseqs  28186  lfgrnloop  29070  numclwlk2lem2f1o  30323  cnlnadjlem5  32015  2ndresdju  32593  nfesum1  34013  nfesum2  34014  ballotlem7  34510  bnj1230  34775  bnj1476  34820  bnj900  34902  bnj958  34913  bnj1000  34914  bnj1014  34934  bnj1123  34959  bnj1307  34996  bnj1321  35000  bnj1384  35005  bnj1398  35007  bnj1408  35009  bnj1444  35016  bnj1445  35017  bnj1446  35018  bnj1447  35019  bnj1448  35020  bnj1449  35021  bnj1466  35026  bnj1467  35027  bnj1518  35037  bnj1519  35038  bnj1520  35039  bnj1525  35042  bnj1523  35044  cvmcov  35246  nfwsuc  35802  nfwlim  35806  nfaltop  35964  currysetlem1  36931  topdifinfindis  37330  rdgssun  37362  exrecfnlem  37363  finxpreclem6  37380  sdclem1  37733  riotasv2s  38947  cdleme26ee  40349  cdlemefs32sn1aw  40403  cdleme43fsv1snlem  40409  cdleme41sn3a  40422  cdleme32d  40433  cdleme32f  40435  cdleme40m  40456  cdleme40n  40457  ltrniotaval  40570  cdlemksv2  40836  cdlemkuv2  40856  cdlemk36  40902  cdlemk38  40904  cdlemkid  40925  cdlemk19x  40932  cdlemk11t  40935  areaquad  43199  nfscott  44222  nfcoll  44239  binomcxplemdvbinom  44336  binomcxplemdvsum  44338  binomcxplemnotnn0  44339  refsum2cnlem1  45025  eliuniincex  45097  disjrnmpt2  45176  rnmptssbi  45248  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  49681