Theorem nfcxfr 2896

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

Syntax hints:   = wceq 1540  Ⅎwnfc 2883

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-cleq 2727  df-clel 2809  df-nfc 2885

This theorem is referenced by:  nfrab1  3436  nfrabw  3454  nfrabwOLD  3455  nfrab  3457  nfdifOLD  4105  nfunOLD  4146  nfinOLD  4200  nfsymdif  4232  nfpw  4594  nfpr  4668  nfsn  4683  nfop  4865  nfint  4932  nfiun  4999  nfiin  5000  nfiung  5001  nfiing  5002  nfiu1OLD  5004  nfii1  5005  nfopab1  5189  nfopab2  5190  nfmpt  5219  nfmpt1  5220  nfxp  5687  nfco  5845  nfcnv  5858  nfdm  5931  nfrn  5932  nfres  5968  nfima  6055  nfpred  6295  nfsuc  6425  nfiota1  6485  nffv  6885  fvmptss  6997  fvmptf  7006  fvopab5  7018  ralrnmptw  7083  ralrnmpt  7085  f1ompt  7100  fompt  7107  f1mpt  7253  fliftfun  7304  nfriota1  7367  riotaprop  7387  nfoprab1  7466  nfoprab2  7467  nfoprab3  7468  nfoprab  7469  nfmpo1  7485  nfmpo2  7486  nfmpo  7487  ovmpos  7553  ov2gf  7554  ov3  7568  nfof  7675  nfofr  7676  nftpos  8258  fvmpocurryd  8268  nffrecs  8280  nfwrecs  8313  nfwrecsOLD  8314  nfrecs  8387  nfrdg  8426  rdgsucmptf  8440  rdgsucmptnf  8441  frsucmpt  8450  frsucmptn  8451  nfixpw  8928  nfixp  8929  nfixp1  8930  xpcomco  9074  nfsup  9461  nfinf  9493  nfoi  9526  cnfcom3clem  9717  ttrclselem1  9737  ttrclselem2  9738  nfdju  9919  dfac8clem  10044  iunfo  10551  pwfseqlem2  10671  pwfseqlem4a  10673  pwfseqlem4  10674  reclem2pr  11060  nfseq  14027  nfwrd  14559  nfsum1  15704  nfsum  15705  nfcprod1  15922  nfcprod  15923  symgval  19350  ptbasfi  23517  mbfsup  25615  itg1climres  25665  itg2splitlem  25699  itg2split  25700  nfitg1  25725  nfitg  25726  lgamgulm2  26996  lgseisenlem2  27337  nosupbnd2  27678  noinfbnd2  27693  nfseqs  28210  lfgrnloop  29050  numclwlk2lem2f1o  30306  cnlnadjlem5  31998  2ndresdju  32573  nfesum1  34017  nfesum2  34018  ballotlem7  34514  bnj1230  34779  bnj1476  34824  bnj900  34906  bnj958  34917  bnj1000  34918  bnj1014  34938  bnj1123  34963  bnj1307  35000  bnj1321  35004  bnj1384  35009  bnj1398  35011  bnj1408  35013  bnj1444  35020  bnj1445  35021  bnj1446  35022  bnj1447  35023  bnj1448  35024  bnj1449  35025  bnj1466  35030  bnj1467  35031  bnj1518  35041  bnj1519  35042  bnj1520  35043  bnj1525  35046  bnj1523  35048  cvmcov  35231  nfwsuc  35782  nfwlim  35786  nfaltop  35944  currysetlem1  36911  topdifinfindis  37310  rdgssun  37342  exrecfnlem  37343  finxpreclem6  37360  sdclem1  37713  riotasv2s  38922  cdleme26ee  40325  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme41sn3a  40398  cdleme32d  40409  cdleme32f  40411  cdleme40m  40432  cdleme40n  40433  ltrniotaval  40546  cdlemksv2  40812  cdlemkuv2  40832  cdlemk36  40878  cdlemk38  40880  cdlemkid  40901  cdlemk19x  40908  cdlemk11t  40911  areaquad  43187  nfscott  44211  nfcoll  44228  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  refsum2cnlem1  45009  eliuniincex  45081  disjrnmpt2  45160  rnmptssbi  45232  allbutfi  45368  allbutfiinf  45395  rexanuz2nf  45467  fmuldfeqlem1  45559  fmuldfeq  45560  mullimc  45593  idlimc  45603  limcperiod  45605  neglimc  45624  addlimc  45625  0ellimcdiv  45626  fnlimcnv  45644  fnlimfvre  45651  fnlimfvre2  45654  fnlimf  45655  fnlimabslt  45656  xlimmnfmpt  45820  xlimpnfmpt  45821  cncfmptssg  45848  cncfshift  45851  cncficcgt0  45865  cncfiooicclem1  45870  dvnmul  45920  dvnprodlem1  45923  itgsinexplem1  45931  itgsubsticclem  45952  stoweidlem14  45991  stoweidlem16  45993  stoweidlem18  45995  stoweidlem22  45999  stoweidlem26  46003  stoweidlem27  46004  stoweidlem31  46008  stoweidlem32  46009  stoweidlem34  46011  stoweidlem35  46012  stoweidlem40  46017  stoweidlem41  46018  stoweidlem42  46019  stoweidlem44  46021  stoweidlem45  46022  stoweidlem46  46023  stoweidlem47  46024  stoweidlem48  46025  stoweidlem50  46027  stoweidlem51  46028  stoweidlem52  46029  stoweidlem53  46030  stoweidlem54  46031  stoweidlem57  46034  stoweidlem59  46036  stoweidlem62  46039  wallispilem5  46046  stirlinglem4  46054  stirlinglem5  46055  stirlinglem8  46058  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  fourierdlem20  46104  fourierdlem31  46115  fourierdlem68  46151  fourierdlem80  46163  fourierdlem89  46172  fourierdlem91  46174  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem115  46198  fourierd  46199  fourierclimd  46200  etransclem48  46259  iundjiun  46437  meaiuninc3v  46461  ovnlerp  46539  ovncvrrp  46541  ovnhoilem1  46578  opnvonmbllem1  46609  iunhoiioolem  46652  vonioo  46659  vonicc  46662  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  issmff  46711  incsmflem  46718  smfpimltxr  46724  smfconst  46726  decsmflem  46743  smfpreimagtf  46745  smflimlem2  46749  smflim  46754  smfpimgtxr  46757  smfresal  46765  smfmullem2  46769  smfmullem4  46771  smfpimbor1lem2  46776  smflim2  46783  smfpimcclem  46784  smflimmpt  46787  smfsup  46791  smfsupmpt  46792  smfsupxr  46793  smfinf  46795  smfinfmpt  46796  smflimsuplem2  46798  smflimsuplem5  46801  smflimsup  46805  smfliminf  46808  smfpimne2  46817  smfdivdmmbl2  46818  fsupdm  46819  fsupdm2  46820  finfdm  46823  finfdm2  46824  nfafv  47113  nfaov  47156  nfafv2  47195  prmdvdsfmtnof1lem1  47546  nfsetrecs  49498