Theorem nfcxfr 2897

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

Syntax hints:   = wceq 1542  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfrab1  3421  nfrabw  3438  nfrab  3440  nfdifOLD  4084  nfunOLD  4125  nfinOLD  4179  nfsymdif  4211  nfpw  4575  nfpr  4651  nfsn  4666  nfop  4847  nfint  4914  nfiun  4980  nfiin  4981  nfiung  4982  nfiing  4983  nfiu1OLD  4985  nfii1  4986  nfopab1  5170  nfopab2  5171  nfmpt  5198  nfmpt1  5199  nfxp  5667  nfco  5824  nfcnv  5837  nfdm  5910  nfrn  5911  nfres  5950  nfima  6037  nfpred  6274  nfsuc  6401  nfiota1  6460  nffv  6854  fvmptss  6964  fvmptf  6973  fvopab5  6985  ralrnmptw  7050  ralrnmpt  7052  f1ompt  7067  fompt  7074  f1mpt  7219  fliftfun  7270  nfriota1  7334  riotaprop  7354  nfoprab1  7431  nfoprab2  7432  nfoprab3  7433  nfoprab  7434  nfmpo1  7450  nfmpo2  7451  nfmpo  7452  ovmpos  7518  ov2gf  7519  ov3  7533  nfof  7640  nfofr  7641  nftpos  8215  fvmpocurryd  8225  nffrecs  8237  nfwrecs  8268  nfrecs  8318  nfrdg  8357  rdgsucmptf  8371  rdgsucmptnf  8372  frsucmpt  8381  frsucmptn  8382  nfixpw  8868  nfixp  8869  nfixp1  8870  xpcomco  9009  nfsup  9368  nfinf  9400  nfoi  9433  cnfcom3clem  9628  ttrclselem1  9648  ttrclselem2  9649  nfdju  9833  dfac8clem  9956  iunfo  10463  pwfseqlem2  10584  pwfseqlem4a  10586  pwfseqlem4  10587  reclem2pr  10973  nfseq  13948  nfwrd  14480  nfsum1  15627  nfsum  15628  nfcprod1  15845  nfcprod  15846  symgval  19317  ptbasfi  23542  mbfsup  25638  itg1climres  25688  itg2splitlem  25722  itg2split  25723  nfitg1  25748  nfitg  25749  lgamgulm2  27019  lgseisenlem2  27360  nosupbnd2  27701  noinfbnd2  27716  nfseqs  28300  lfgrnloop  29216  numclwlk2lem2f1o  30472  cnlnadjlem5  32165  2ndresdju  32745  nfesum1  34224  nfesum2  34225  ballotlem7  34720  bnj1230  34984  bnj1476  35029  bnj900  35111  bnj958  35122  bnj1000  35123  bnj1014  35143  bnj1123  35168  bnj1307  35205  bnj1321  35209  bnj1384  35214  bnj1398  35216  bnj1408  35218  bnj1444  35225  bnj1445  35226  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1449  35230  bnj1466  35235  bnj1467  35236  bnj1518  35246  bnj1519  35247  bnj1520  35248  bnj1525  35251  bnj1523  35253  cvmcov  35485  nfwsuc  36038  nfwlim  36042  nfaltop  36202  currysetlem1  37222  topdifinfindis  37628  rdgssun  37660  exrecfnlem  37661  finxpreclem6  37678  sdclem1  38023  riotasv2s  39363  cdleme26ee  40765  cdlemefs32sn1aw  40819  cdleme43fsv1snlem  40825  cdleme41sn3a  40838  cdleme32d  40849  cdleme32f  40851  cdleme40m  40872  cdleme40n  40873  ltrniotaval  40986  cdlemksv2  41252  cdlemkuv2  41272  cdlemk36  41318  cdlemk38  41320  cdlemkid  41341  cdlemk19x  41348  cdlemk11t  41351  areaquad  43602  nfscott  44624  nfcoll  44641  binomcxplemdvbinom  44738  binomcxplemdvsum  44740  binomcxplemnotnn0  44741  refsum2cnlem1  45426  eliuniincex  45497  disjrnmpt2  45576  rnmptssbi  45647  allbutfi  45780  allbutfiinf  45807  rexanuz2nf  45879  fmuldfeqlem1  45971  fmuldfeq  45972  mullimc  46005  idlimc  46015  limcperiod  46017  neglimc  46034  addlimc  46035  0ellimcdiv  46036  fnlimcnv  46054  fnlimfvre  46061  fnlimfvre2  46064  fnlimf  46065  fnlimabslt  46066  xlimmnfmpt  46230  xlimpnfmpt  46231  cncfmptssg  46258  cncfshift  46261  cncficcgt0  46275  cncfiooicclem1  46280  dvnmul  46330  dvnprodlem1  46333  itgsinexplem1  46341  itgsubsticclem  46362  stoweidlem14  46401  stoweidlem16  46403  stoweidlem18  46405  stoweidlem22  46409  stoweidlem26  46413  stoweidlem27  46414  stoweidlem31  46418  stoweidlem32  46419  stoweidlem34  46421  stoweidlem35  46422  stoweidlem40  46427  stoweidlem41  46428  stoweidlem42  46429  stoweidlem44  46431  stoweidlem45  46432  stoweidlem46  46433  stoweidlem47  46434  stoweidlem48  46435  stoweidlem50  46437  stoweidlem51  46438  stoweidlem52  46439  stoweidlem53  46440  stoweidlem54  46441  stoweidlem57  46444  stoweidlem59  46446  stoweidlem62  46449  wallispilem5  46456  stirlinglem4  46464  stirlinglem5  46465  stirlinglem8  46468  stirlinglem11  46471  stirlinglem12  46472  stirlinglem13  46473  stirlinglem14  46474  stirlinglem15  46475  fourierdlem20  46514  fourierdlem31  46525  fourierdlem68  46561  fourierdlem80  46573  fourierdlem89  46582  fourierdlem91  46584  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem115  46608  fourierd  46609  fourierclimd  46610  etransclem48  46669  iundjiun  46847  meaiuninc3v  46871  ovnlerp  46949  ovncvrrp  46951  ovnhoilem1  46988  opnvonmbllem1  47019  iunhoiioolem  47062  vonioo  47069  vonicc  47072  pimdecfgtioc  47102  pimincfltioc  47103  pimdecfgtioo  47104  pimincfltioo  47105  issmff  47121  incsmflem  47128  smfpimltxr  47134  smfconst  47136  decsmflem  47153  smfpreimagtf  47155  smflimlem2  47159  smflim  47164  smfpimgtxr  47167  smfresal  47175  smfmullem2  47179  smfmullem4  47181  smfpimbor1lem2  47186  smflim2  47193  smfpimcclem  47194  smflimmpt  47197  smfsup  47201  smfsupmpt  47202  smfsupxr  47203  smfinf  47205  smfinfmpt  47206  smflimsuplem2  47208  smflimsuplem5  47211  smflimsup  47215  smfliminf  47218  smfpimne2  47227  smfdivdmmbl2  47228  fsupdm  47229  fsupdm2  47230  finfdm  47233  finfdm2  47234  nfafv  47525  nfaov  47568  nfafv2  47607  prmdvdsfmtnof1lem1  47973  nfsetrecs  50074