Theorem nfcxfr 2947

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

Syntax hints:   = wceq 1522  Ⅎwnfc 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-nf 1766  df-cleq 2788  df-clel 2863  df-nfc 2935

This theorem is referenced by:  nfrab1  3344  nfrab  3345  nfdif  4023  nfun  4062  nfin  4113  nfsymdif  4143  nfpw  4467  nfpr  4535  nfsn  4550  nfop  4726  nfuni  4751  nfint  4792  nfiun  4854  nfiin  4855  nfiu1  4856  nfii1  4857  nfopab  5030  nfopab1  5031  nfopab2  5032  nfmpt  5057  nfmpt1  5058  nfxp  5476  nfco  5622  nfcnv  5635  nfdm  5705  nfrn  5706  nfres  5736  nfima  5814  nfpred  6028  nfsuc  6137  nfiota1  6191  nffv  6548  fvmptss  6646  fvmptf  6655  fvopab5  6665  ralrnmpt  6725  f1ompt  6738  f1mpt  6884  fliftfun  6928  nfriota1  6984  riotaprop  7001  nfoprab1  7074  nfoprab2  7075  nfoprab3  7076  nfoprab  7077  nfmpo1  7092  nfmpo2  7093  nfmpo  7094  ovmpos  7154  ov2gf  7155  ov3  7167  nfof  7272  nfofr  7273  nftpos  7778  fvmpocurryd  7788  nfwrecs  7800  nfrecs  7863  nfrdg  7902  rdgsucmptf  7916  rdgsucmptnf  7917  frsucmpt  7925  frsucmptn  7926  nfixp  8329  nfixp1  8330  xpcomco  8454  nfsup  8761  nfinf  8792  nfoi  8824  cnfcom3clem  9014  nfdju  9182  dfac8clem  9304  iunfo  9807  pwfseqlem2  9927  pwfseqlem4a  9929  pwfseqlem4  9930  reclem2pr  10316  nfseq  13229  nfwrd  13740  nfsum1  14880  nfsum  14881  nfcprod1  15097  nfcprod  15098  ptbasfi  21873  mbfsup  23948  itg1climres  23998  itg2splitlem  24032  itg2split  24033  nfitg1  24057  nfitg  24058  lgamgulm2  25295  lgseisenlem2  25634  lfgrnloop  26593  numclwlk2lem2f1o  27850  cnlnadjlem5  29539  nfesum1  30916  nfesum2  30917  ballotlem7  31410  bnj1230  31691  bnj1476  31735  bnj900  31817  bnj958  31828  bnj1000  31829  bnj1014  31848  bnj1123  31872  bnj1307  31909  bnj1321  31913  bnj1384  31918  bnj1398  31920  bnj1408  31922  bnj1444  31929  bnj1445  31930  bnj1446  31931  bnj1447  31932  bnj1448  31933  bnj1449  31934  bnj1466  31939  bnj1467  31940  bnj1518  31950  bnj1519  31951  bnj1520  31952  bnj1525  31955  bnj1523  31957  cvmcov  32118  nfwsuc  32714  nfwlim  32718  nffrecs  32729  nosupbnd2  32825  nfaltop  33050  currysetlem1  33829  topdifinfindis  34158  rdgssun  34190  exrecfnlem  34191  finxpreclem6  34208  sdclem1  34550  riotasv2s  35625  cdleme26ee  37027  cdlemefs32sn1aw  37081  cdleme43fsv1snlem  37087  cdleme41sn3a  37100  cdleme32d  37111  cdleme32f  37113  cdleme40m  37134  cdleme40n  37135  ltrniotaval  37248  cdlemksv2  37514  cdlemkuv2  37534  cdlemk36  37580  cdlemk38  37582  cdlemkid  37603  cdlemk19x  37610  cdlemk11t  37613  areaquad  39308  nfscott  40072  nfcoll  40089  binomcxplemdvbinom  40223  binomcxplemdvsum  40225  binomcxplemnotnn0  40226  refsum2cnlem1  40833  eliuniincex  40915  suprnmpt  40970  disjrnmpt2  40989  fompt  40993  rnmptssbi  41075  allbutfi  41206  allbutfiinf  41236  fmuldfeqlem1  41405  fmuldfeq  41406  mullimc  41439  idlimc  41449  limcperiod  41451  neglimc  41470  addlimc  41471  0ellimcdiv  41472  fnlimcnv  41490  fnlimfvre  41497  fnlimfvre2  41500  fnlimf  41501  fnlimabslt  41502  xlimmnfmpt  41666  xlimpnfmpt  41667  cncfmptssg  41694  cncfshift  41698  cncficcgt0  41712  cncfiooicclem1  41717  dvnmul  41769  dvnprodlem1  41772  itgsinexplem1  41780  itgsubsticclem  41801  stoweidlem14  41841  stoweidlem16  41843  stoweidlem18  41845  stoweidlem22  41849  stoweidlem26  41853  stoweidlem27  41854  stoweidlem31  41858  stoweidlem32  41859  stoweidlem34  41861  stoweidlem35  41862  stoweidlem40  41867  stoweidlem41  41868  stoweidlem42  41869  stoweidlem44  41871  stoweidlem45  41872  stoweidlem46  41873  stoweidlem47  41874  stoweidlem48  41875  stoweidlem50  41877  stoweidlem51  41878  stoweidlem52  41879  stoweidlem53  41880  stoweidlem54  41881  stoweidlem57  41884  stoweidlem59  41886  stoweidlem62  41889  wallispilem5  41896  stirlinglem4  41904  stirlinglem5  41905  stirlinglem8  41908  stirlinglem11  41911  stirlinglem12  41912  stirlinglem13  41913  stirlinglem14  41914  stirlinglem15  41915  fourierdlem20  41954  fourierdlem31  41965  fourierdlem68  42001  fourierdlem80  42013  fourierdlem89  42022  fourierdlem91  42024  fourierdlem103  42036  fourierdlem104  42037  fourierdlem112  42045  fourierdlem115  42048  fourierd  42049  fourierclimd  42050  etransclem48  42109  iundjiun  42284  meaiuninc3v  42308  ovnlerp  42386  ovncvrrp  42388  ovnhoilem1  42425  opnvonmbllem1  42456  iunhoiioolem  42499  vonioo  42506  vonicc  42509  pimdecfgtioc  42535  pimincfltioc  42536  pimdecfgtioo  42537  pimincfltioo  42538  issmff  42553  incsmflem  42560  smfconst  42568  decsmflem  42584  smfpreimagtf  42586  smflimlem2  42590  smflim  42595  smfpimgtxr  42598  smfresal  42605  smfmullem2  42609  smfmullem4  42611  smfpimbor1lem2  42616  smflim2  42622  smfpimcclem  42623  smflimmpt  42626  smfsup  42630  smfsupmpt  42631  smfsupxr  42632  smfinf  42634  smfinfmpt  42635  smflimsuplem2  42637  smflimsuplem5  42640  smflimsup  42644  smfliminf  42647  nfafv  42851  nfaov  42894  nfafv2  42933  prmdvdsfmtnof1lem1  43228  nfsetrecs  44269