Theorem nfcxfr 2926

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

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnfc 2913

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-cleq 2758  df-clel 2841  df-nfc 2915

This theorem is used by:  nfrab1  3439  nfrabw  3455  nfrab  3456  nfsymdif  4213  nfpw  4586  nfpr  4663  nfsn  4678  nfop  4859  nfint  4927  nfiun  4993  nfiin  4994  nfiung  4995  nfiing  4996  nfii1  4998  nfopab1  5186  nfopab2  5187  nfmpt  5214  nfmpt1  5215  nfxp  5699  nfco  5856  nfcnv  5869  nfdm  5946  nfrn  5947  nfres  5985  nfima  6075  nfpred  6314  nfsuc  6442  nfiota1  6501  nffv  6898  fvmptss  7009  fvmptf  7018  fvopab5  7030  ralrnmptw  7096  ralrnmpt  7098  f1ompt  7113  fompt  7120  f1mpt  7266  fliftfun  7321  nfriota1  7387  riotaprop  7407  nfoprab1  7484  nfoprab2  7485  nfoprab3  7486  nfoprab  7487  nfmpo1  7503  nfmpo2  7504  nfmpo  7505  ovmpos  7571  ov2gf  7572  ov3  7586  nfof  7693  nfofr  7694  nftpos  8266  fvmpocurryd  8276  nffrecs  8289  nfwrecs  8320  nfrecs  8370  nfrdg  8410  rdgsucmptf  8424  rdgsucmptnf  8425  frsucmpt  8434  frsucmptn  8435  nfixpw  8923  nfixp  8924  nfixp1  8925  xpcomco  9065  nfsup  9421  nfinf  9453  nfoi  9486  cnfcom3clem  9684  ttrclselem1  9704  ttrclselem2  9705  nfscott  9871  nfdju  9912  dfac8clem  10035  iunfo  10541  pwfseqlem2  10662  pwfseqlem4a  10664  pwfseqlem4  10665  reclem2pr  11051  nfseq  14067  nfwrd  14600  nfsum1  15767  nfsum  15768  nfcprod1  15988  nfcprod  15989  symgval  19472  ptbasfi  23775  mbfsup  25860  itg1climres  25910  itg2splitlem  25944  itg2split  25945  nfitg1  25970  nfitg  25971  lgamgulm2  27237  lgseisenlem2  27577  nosupbnd2  27917  noinfbnd2  27932  nfseqs  28517  lfgrnloop  29512  numclwlk2lem2f1o  30767  cnlnadjlem5  32460  2ndresdju  33031  nfesum1  34461  nfesum2  34462  ballotlem7  34957  bnj1230  35221  bnj1476  35266  bnj900  35348  bnj958  35359  bnj1000  35360  bnj1014  35380  bnj1123  35405  bnj1307  35442  bnj1321  35446  bnj1384  35451  bnj1398  35453  bnj1408  35455  bnj1444  35462  bnj1445  35463  bnj1446  35464  bnj1447  35465  bnj1448  35466  bnj1449  35467  bnj1466  35472  bnj1467  35473  bnj1518  35483  bnj1519  35484  bnj1520  35485  bnj1525  35488  bnj1523  35490  cvmcov  35775  nfwsuc  36328  nfwlim  36332  nfaltop  36492  nfttc  37042  currysetlem1  37623  topdifinfindis  38032  rdgssun  38064  exrecfnlem  38065  finxpreclem6  38082  sdclem1  38434  riotasv2s  39772  cdleme26ee  41174  cdlemefs32sn1aw  41228  cdleme43fsv1snlem  41234  cdleme41sn3a  41247  cdleme32d  41258  cdleme32f  41260  cdleme40m  41281  cdleme40n  41282  ltrniotaval  41395  cdlemksv2  41661  cdlemkuv2  41681  cdlemk36  41727  cdlemk38  41729  cdlemkid  41750  cdlemk19x  41757  cdlemk11t  41760  areaquad  43983  nfcoll  45006  binomcxplemdvbinom  45103  binomcxplemdvsum  45105  binomcxplemnotnn0  45106  refsum2cnlem1  45797  eliuniincex  45867  disjrnmpt2  45946  rnmptssbi  46015  allbutfi  46148  allbutfiinf  46174  rexanuz2nf  46246  fmuldfeqlem1  46338  fmuldfeq  46339  mullimc  46372  idlimc  46382  limcperiod  46384  neglimc  46401  addlimc  46402  0ellimcdiv  46403  fnlimcnv  46421  fnlimfvre  46428  fnlimfvre2  46431  fnlimf  46432  fnlimabslt  46433  xlimmnfmpt  46597  xlimpnfmpt  46598  cncfmptssg  46625  cncfshift  46628  cncficcgt0  46642  cncfiooicclem1  46647  dvnmul  46697  dvnprodlem1  46700  itgsinexplem1  46708  itgsubsticclem  46729  stoweidlem14  46768  stoweidlem16  46770  stoweidlem18  46772  stoweidlem22  46776  stoweidlem26  46780  stoweidlem27  46781  stoweidlem31  46785  stoweidlem32  46786  stoweidlem34  46788  stoweidlem35  46789  stoweidlem40  46794  stoweidlem41  46795  stoweidlem42  46796  stoweidlem44  46798  stoweidlem45  46799  stoweidlem46  46800  stoweidlem47  46801  stoweidlem48  46802  stoweidlem50  46804  stoweidlem51  46805  stoweidlem52  46806  stoweidlem53  46807  stoweidlem54  46808  stoweidlem57  46811  stoweidlem59  46813  stoweidlem62  46816  wallispilem5  46823  stirlinglem4  46831  stirlinglem5  46832  stirlinglem8  46835  stirlinglem11  46838  stirlinglem12  46839  stirlinglem13  46840  stirlinglem14  46841  stirlinglem15  46842  fourierdlem20  46881  fourierdlem31  46892  fourierdlem68  46928  fourierdlem80  46940  fourierdlem89  46949  fourierdlem91  46951  fourierdlem103  46963  fourierdlem104  46964  fourierdlem112  46972  fourierdlem115  46975  fourierd  46976  fourierclimd  46977  etransclem48  47036  iundjiun  47214  meaiuninc3v  47238  ovnlerp  47316  ovncvrrp  47318  ovnhoilem1  47355  opnvonmbllem1  47386  iunhoiioolem  47429  vonioo  47436  vonicc  47439  pimdecfgtioc  47469  pimincfltioc  47470  pimdecfgtioo  47471  pimincfltioo  47472  issmff  47488  incsmflem  47495  smfpimltxr  47501  smfconst  47503  decsmflem  47520  smfpreimagtf  47522  smflimlem2  47526  smflim  47531  smfpimgtxr  47534  smfresal  47542  smfmullem2  47546  smfmullem4  47548  smfpimbor1lem2  47553  smflim2  47560  smfpimcclem  47561  smflimmpt  47564  smfsup  47568  smfsupmpt  47569  smfsupxr  47570  smfinf  47572  smfinfmpt  47573  smflimsuplem2  47575  smflimsuplem5  47578  smflimsup  47582  smfliminf  47585  smfpimne2  47594  smfdivdmmbl2  47595  fsupdm  47596  fsupdm2  47597  finfdm  47600  finfdm2  47601  nfafv  47913  nfaov  47956  nfafv2  47995  prmdvdsfmtnof1lem1  48376  nfsetrecs  50504