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  28188  lfgrnloop  29074  numclwlk2lem2f1o  30327  cnlnadjlem5  32019  2ndresdju  32600  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  35256  nfwsuc  35812  nfwlim  35816  nfaltop  35974  currysetlem1  36941  topdifinfindis  37340  rdgssun  37372  exrecfnlem  37373  finxpreclem6  37390  sdclem1  37743  riotasv2s  38957  cdleme26ee  40359  cdlemefs32sn1aw  40413  cdleme43fsv1snlem  40419  cdleme41sn3a  40432  cdleme32d  40443  cdleme32f  40445  cdleme40m  40466  cdleme40n  40467  ltrniotaval  40580  cdlemksv2  40846  cdlemkuv2  40866  cdlemk36  40912  cdlemk38  40914  cdlemkid  40935  cdlemk19x  40942  cdlemk11t  40945  areaquad  43209  nfscott  44232  nfcoll  44249  binomcxplemdvbinom  44346  binomcxplemdvsum  44348  binomcxplemnotnn0  44349  refsum2cnlem1  45035  eliuniincex  45107  disjrnmpt2  45186  rnmptssbi  45258  allbutfi  45392  allbutfiinf  45419  rexanuz2nf  45491  fmuldfeqlem1  45583  fmuldfeq  45584  mullimc  45617  idlimc  45627  limcperiod  45629  neglimc  45648  addlimc  45649  0ellimcdiv  45650  fnlimcnv  45668  fnlimfvre  45675  fnlimfvre2  45678  fnlimf  45679  fnlimabslt  45680  xlimmnfmpt  45844  xlimpnfmpt  45845  cncfmptssg  45872  cncfshift  45875  cncficcgt0  45889  cncfiooicclem1  45894  dvnmul  45944  dvnprodlem1  45947  itgsinexplem1  45955  itgsubsticclem  45976  stoweidlem14  46015  stoweidlem16  46017  stoweidlem18  46019  stoweidlem22  46023  stoweidlem26  46027  stoweidlem27  46028  stoweidlem31  46032  stoweidlem32  46033  stoweidlem34  46035  stoweidlem35  46036  stoweidlem40  46041  stoweidlem41  46042  stoweidlem42  46043  stoweidlem44  46045  stoweidlem45  46046  stoweidlem46  46047  stoweidlem47  46048  stoweidlem48  46049  stoweidlem50  46051  stoweidlem51  46052  stoweidlem52  46053  stoweidlem53  46054  stoweidlem54  46055  stoweidlem57  46058  stoweidlem59  46060  stoweidlem62  46063  wallispilem5  46070  stirlinglem4  46078  stirlinglem5  46079  stirlinglem8  46082  stirlinglem11  46085  stirlinglem12  46086  stirlinglem13  46087  stirlinglem14  46088  stirlinglem15  46089  fourierdlem20  46128  fourierdlem31  46139  fourierdlem68  46175  fourierdlem80  46187  fourierdlem89  46196  fourierdlem91  46198  fourierdlem103  46210  fourierdlem104  46211  fourierdlem112  46219  fourierdlem115  46222  fourierd  46223  fourierclimd  46224  etransclem48  46283  iundjiun  46461  meaiuninc3v  46485  ovnlerp  46563  ovncvrrp  46565  ovnhoilem1  46602  opnvonmbllem1  46633  iunhoiioolem  46676  vonioo  46683  vonicc  46686  pimdecfgtioc  46716  pimincfltioc  46717  pimdecfgtioo  46718  pimincfltioo  46719  issmff  46735  incsmflem  46742  smfpimltxr  46748  smfconst  46750  decsmflem  46767  smfpreimagtf  46769  smflimlem2  46773  smflim  46778  smfpimgtxr  46781  smfresal  46789  smfmullem2  46793  smfmullem4  46795  smfpimbor1lem2  46800  smflim2  46807  smfpimcclem  46808  smflimmpt  46811  smfsup  46815  smfsupmpt  46816  smfsupxr  46817  smfinf  46819  smfinfmpt  46820  smflimsuplem2  46822  smflimsuplem5  46825  smflimsup  46829  smfliminf  46832  smfpimne2  46841  smfdivdmmbl2  46842  fsupdm  46843  fsupdm2  46844  finfdm  46847  finfdm2  46848  nfafv  47140  nfaov  47183  nfafv2  47222  prmdvdsfmtnof1lem1  47588  nfsetrecs  49691