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  3410  nfrabw  3427  nfrab  3428  nfdifOLD  4071  nfunOLD  4112  nfinOLD  4166  nfsymdif  4198  nfpw  4561  nfpr  4637  nfsn  4652  nfop  4833  nfint  4900  nfiun  4966  nfiin  4967  nfiung  4968  nfiing  4969  nfiu1OLD  4971  nfii1  4972  nfopab1  5156  nfopab2  5157  nfmpt  5184  nfmpt1  5185  nfxp  5659  nfco  5816  nfcnv  5829  nfdm  5902  nfrn  5903  nfres  5942  nfima  6029  nfpred  6266  nfsuc  6393  nfiota1  6452  nffv  6846  fvmptss  6956  fvmptf  6965  fvopab5  6977  ralrnmptw  7042  ralrnmpt  7044  f1ompt  7059  fompt  7066  f1mpt  7211  fliftfun  7262  nfriota1  7326  riotaprop  7346  nfoprab1  7423  nfoprab2  7424  nfoprab3  7425  nfoprab  7426  nfmpo1  7442  nfmpo2  7443  nfmpo  7444  ovmpos  7510  ov2gf  7511  ov3  7525  nfof  7632  nfofr  7633  nftpos  8206  fvmpocurryd  8216  nffrecs  8228  nfwrecs  8259  nfrecs  8309  nfrdg  8348  rdgsucmptf  8362  rdgsucmptnf  8363  frsucmpt  8372  frsucmptn  8373  nfixpw  8859  nfixp  8860  nfixp1  8861  xpcomco  9000  nfsup  9359  nfinf  9391  nfoi  9424  cnfcom3clem  9621  ttrclselem1  9641  ttrclselem2  9642  nfdju  9826  dfac8clem  9949  iunfo  10456  pwfseqlem2  10577  pwfseqlem4a  10579  pwfseqlem4  10580  reclem2pr  10966  nfseq  13968  nfwrd  14500  nfsum1  15647  nfsum  15648  nfcprod1  15868  nfcprod  15869  symgval  19341  ptbasfi  23560  mbfsup  25645  itg1climres  25695  itg2splitlem  25729  itg2split  25730  nfitg1  25755  nfitg  25756  lgamgulm2  27017  lgseisenlem2  27357  nosupbnd2  27698  noinfbnd2  27713  nfseqs  28297  lfgrnloop  29212  numclwlk2lem2f1o  30468  cnlnadjlem5  32161  2ndresdju  32741  nfesum1  34204  nfesum2  34205  ballotlem7  34700  bnj1230  34964  bnj1476  35009  bnj900  35091  bnj958  35102  bnj1000  35103  bnj1014  35123  bnj1123  35148  bnj1307  35185  bnj1321  35189  bnj1384  35194  bnj1398  35196  bnj1408  35198  bnj1444  35205  bnj1445  35206  bnj1446  35207  bnj1447  35208  bnj1448  35209  bnj1449  35210  bnj1466  35215  bnj1467  35216  bnj1518  35226  bnj1519  35227  bnj1520  35228  bnj1525  35231  bnj1523  35233  cvmcov  35465  nfwsuc  36018  nfwlim  36022  nfaltop  36182  nfttc  36693  currysetlem1  37274  topdifinfindis  37682  rdgssun  37714  exrecfnlem  37715  finxpreclem6  37732  sdclem1  38084  riotasv2s  39424  cdleme26ee  40826  cdlemefs32sn1aw  40880  cdleme43fsv1snlem  40886  cdleme41sn3a  40899  cdleme32d  40910  cdleme32f  40912  cdleme40m  40933  cdleme40n  40934  ltrniotaval  41047  cdlemksv2  41313  cdlemkuv2  41333  cdlemk36  41379  cdlemk38  41381  cdlemkid  41402  cdlemk19x  41409  cdlemk11t  41412  areaquad  43668  nfscott  44690  nfcoll  44707  binomcxplemdvbinom  44804  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  refsum2cnlem1  45492  eliuniincex  45563  disjrnmpt2  45642  rnmptssbi  45713  allbutfi  45846  allbutfiinf  45872  rexanuz2nf  45944  fmuldfeqlem1  46036  fmuldfeq  46037  mullimc  46070  idlimc  46080  limcperiod  46082  neglimc  46099  addlimc  46100  0ellimcdiv  46101  fnlimcnv  46119  fnlimfvre  46126  fnlimfvre2  46129  fnlimf  46130  fnlimabslt  46131  xlimmnfmpt  46295  xlimpnfmpt  46296  cncfmptssg  46323  cncfshift  46326  cncficcgt0  46340  cncfiooicclem1  46345  dvnmul  46395  dvnprodlem1  46398  itgsinexplem1  46406  itgsubsticclem  46427  stoweidlem14  46466  stoweidlem16  46468  stoweidlem18  46470  stoweidlem22  46474  stoweidlem26  46478  stoweidlem27  46479  stoweidlem31  46483  stoweidlem32  46484  stoweidlem34  46486  stoweidlem35  46487  stoweidlem40  46492  stoweidlem41  46493  stoweidlem42  46494  stoweidlem44  46496  stoweidlem45  46497  stoweidlem46  46498  stoweidlem47  46499  stoweidlem48  46500  stoweidlem50  46502  stoweidlem51  46503  stoweidlem52  46504  stoweidlem53  46505  stoweidlem54  46506  stoweidlem57  46509  stoweidlem59  46511  stoweidlem62  46514  wallispilem5  46521  stirlinglem4  46529  stirlinglem5  46530  stirlinglem8  46533  stirlinglem11  46536  stirlinglem12  46537  stirlinglem13  46538  stirlinglem14  46539  stirlinglem15  46540  fourierdlem20  46579  fourierdlem31  46590  fourierdlem68  46626  fourierdlem80  46638  fourierdlem89  46647  fourierdlem91  46649  fourierdlem103  46661  fourierdlem104  46662  fourierdlem112  46670  fourierdlem115  46673  fourierd  46674  fourierclimd  46675  etransclem48  46734  iundjiun  46912  meaiuninc3v  46936  ovnlerp  47014  ovncvrrp  47016  ovnhoilem1  47053  opnvonmbllem1  47084  iunhoiioolem  47127  vonioo  47134  vonicc  47137  pimdecfgtioc  47167  pimincfltioc  47168  pimdecfgtioo  47169  pimincfltioo  47170  issmff  47186  incsmflem  47193  smfpimltxr  47199  smfconst  47201  decsmflem  47218  smfpreimagtf  47220  smflimlem2  47224  smflim  47229  smfpimgtxr  47232  smfresal  47240  smfmullem2  47244  smfmullem4  47246  smfpimbor1lem2  47251  smflim2  47258  smfpimcclem  47259  smflimmpt  47262  smfsup  47266  smfsupmpt  47267  smfsupxr  47268  smfinf  47270  smfinfmpt  47271  smflimsuplem2  47273  smflimsuplem5  47276  smflimsup  47280  smfliminf  47283  smfpimne2  47292  smfdivdmmbl2  47293  fsupdm  47294  fsupdm2  47295  finfdm  47298  finfdm2  47299  nfafv  47602  nfaov  47645  nfafv2  47684  prmdvdsfmtnof1lem1  48065  nfsetrecs  50179