Theorem nfcxfr 2889

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

Syntax hints:   = wceq 1540  Ⅎwnfc 2876

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878

This theorem is referenced by:  nfrab1  3426  nfrabw  3443  nfrab  3445  nfdifOLD  4093  nfunOLD  4134  nfinOLD  4188  nfsymdif  4220  nfpw  4582  nfpr  4656  nfsn  4671  nfop  4853  nfint  4920  nfiun  4987  nfiin  4988  nfiung  4989  nfiing  4990  nfiu1OLD  4992  nfii1  4993  nfopab1  5177  nfopab2  5178  nfmpt  5205  nfmpt1  5206  nfxp  5671  nfco  5829  nfcnv  5842  nfdm  5915  nfrn  5916  nfres  5952  nfima  6039  nfpred  6279  nfsuc  6406  nfiota1  6466  nffv  6868  fvmptss  6980  fvmptf  6989  fvopab5  7001  ralrnmptw  7066  ralrnmpt  7068  f1ompt  7083  fompt  7090  f1mpt  7236  fliftfun  7287  nfriota1  7351  riotaprop  7371  nfoprab1  7450  nfoprab2  7451  nfoprab3  7452  nfoprab  7453  nfmpo1  7469  nfmpo2  7470  nfmpo  7471  ovmpos  7537  ov2gf  7538  ov3  7552  nfof  7659  nfofr  7660  nftpos  8240  fvmpocurryd  8250  nffrecs  8262  nfwrecs  8293  nfrecs  8343  nfrdg  8382  rdgsucmptf  8396  rdgsucmptnf  8397  frsucmpt  8406  frsucmptn  8407  nfixpw  8889  nfixp  8890  nfixp1  8891  xpcomco  9031  nfsup  9402  nfinf  9434  nfoi  9467  cnfcom3clem  9658  ttrclselem1  9678  ttrclselem2  9679  nfdju  9860  dfac8clem  9985  iunfo  10492  pwfseqlem2  10612  pwfseqlem4a  10614  pwfseqlem4  10615  reclem2pr  11001  nfseq  13976  nfwrd  14508  nfsum1  15656  nfsum  15657  nfcprod1  15874  nfcprod  15875  symgval  19301  ptbasfi  23468  mbfsup  25565  itg1climres  25615  itg2splitlem  25649  itg2split  25650  nfitg1  25675  nfitg  25676  lgamgulm2  26946  lgseisenlem2  27287  nosupbnd2  27628  noinfbnd2  27643  nfseqs  28181  lfgrnloop  29052  numclwlk2lem2f1o  30308  cnlnadjlem5  32000  2ndresdju  32573  nfesum1  34030  nfesum2  34031  ballotlem7  34527  bnj1230  34792  bnj1476  34837  bnj900  34919  bnj958  34930  bnj1000  34931  bnj1014  34951  bnj1123  34976  bnj1307  35013  bnj1321  35017  bnj1384  35022  bnj1398  35024  bnj1408  35026  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1447  35036  bnj1448  35037  bnj1449  35038  bnj1466  35043  bnj1467  35044  bnj1518  35054  bnj1519  35055  bnj1520  35056  bnj1525  35059  bnj1523  35061  cvmcov  35250  nfwsuc  35806  nfwlim  35810  nfaltop  35968  currysetlem1  36935  topdifinfindis  37334  rdgssun  37366  exrecfnlem  37367  finxpreclem6  37384  sdclem1  37737  riotasv2s  38951  cdleme26ee  40354  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme41sn3a  40427  cdleme32d  40438  cdleme32f  40440  cdleme40m  40461  cdleme40n  40462  ltrniotaval  40575  cdlemksv2  40841  cdlemkuv2  40861  cdlemk36  40907  cdlemk38  40909  cdlemkid  40930  cdlemk19x  40937  cdlemk11t  40940  areaquad  43205  nfscott  44228  nfcoll  44245  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  refsum2cnlem1  45031  eliuniincex  45103  disjrnmpt2  45182  rnmptssbi  45254  allbutfi  45389  allbutfiinf  45416  rexanuz2nf  45488  fmuldfeqlem1  45580  fmuldfeq  45581  mullimc  45614  idlimc  45624  limcperiod  45626  neglimc  45645  addlimc  45646  0ellimcdiv  45647  fnlimcnv  45665  fnlimfvre  45672  fnlimfvre2  45675  fnlimf  45676  fnlimabslt  45677  xlimmnfmpt  45841  xlimpnfmpt  45842  cncfmptssg  45869  cncfshift  45872  cncficcgt0  45886  cncfiooicclem1  45891  dvnmul  45941  dvnprodlem1  45944  itgsinexplem1  45952  itgsubsticclem  45973  stoweidlem14  46012  stoweidlem16  46014  stoweidlem18  46016  stoweidlem22  46020  stoweidlem26  46024  stoweidlem27  46025  stoweidlem31  46029  stoweidlem32  46030  stoweidlem34  46032  stoweidlem35  46033  stoweidlem40  46038  stoweidlem41  46039  stoweidlem42  46040  stoweidlem44  46042  stoweidlem45  46043  stoweidlem46  46044  stoweidlem47  46045  stoweidlem48  46046  stoweidlem50  46048  stoweidlem51  46049  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  stoweidlem57  46055  stoweidlem59  46057  stoweidlem62  46060  wallispilem5  46067  stirlinglem4  46075  stirlinglem5  46076  stirlinglem8  46079  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  fourierdlem20  46125  fourierdlem31  46136  fourierdlem68  46172  fourierdlem80  46184  fourierdlem89  46193  fourierdlem91  46195  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem115  46219  fourierd  46220  fourierclimd  46221  etransclem48  46280  iundjiun  46458  meaiuninc3v  46482  ovnlerp  46560  ovncvrrp  46562  ovnhoilem1  46599  opnvonmbllem1  46630  iunhoiioolem  46673  vonioo  46680  vonicc  46683  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  issmff  46732  incsmflem  46739  smfpimltxr  46745  smfconst  46747  decsmflem  46764  smfpreimagtf  46766  smflimlem2  46770  smflim  46775  smfpimgtxr  46778  smfresal  46786  smfmullem2  46790  smfmullem4  46792  smfpimbor1lem2  46797  smflim2  46804  smfpimcclem  46805  smflimmpt  46808  smfsup  46812  smfsupmpt  46813  smfsupxr  46814  smfinf  46816  smfinfmpt  46817  smflimsuplem2  46819  smflimsuplem5  46822  smflimsup  46826  smfliminf  46829  smfpimne2  46838  smfdivdmmbl2  46839  fsupdm  46840  fsupdm2  46841  finfdm  46844  finfdm2  46845  nfafv  47137  nfaov  47180  nfafv2  47219  prmdvdsfmtnof1lem1  47585  nfsetrecs  49675