Theorem nfcxfr 2904

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

Syntax hints:   = wceq 1539  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-cleq 2730  df-clel 2817  df-nfc 2888

This theorem is referenced by:  nfrab1  3310  nfrabw  3311  nfrab  3312  nfdif  4056  nfun  4095  nfin  4147  nfsymdif  4177  nfpw  4551  nfpr  4623  nfsn  4640  nfop  4817  nfint  4886  nfiun  4951  nfiin  4952  nfiung  4953  nfiing  4954  nfiu1  4955  nfii1  4956  nfopab1  5140  nfopab2  5141  nfmpt  5177  nfmpt1  5178  nfxp  5613  nfco  5763  nfcnv  5776  nfdm  5849  nfrn  5850  nfres  5882  nfima  5966  nfpred  6196  nfsuc  6322  nfiota1  6378  nffv  6766  fvmptss  6869  fvmptf  6878  fvopab5  6889  ralrnmptw  6952  ralrnmpt  6954  f1ompt  6967  f1mpt  7115  fliftfun  7163  nfriota1  7219  riotaprop  7240  nfoprab1  7314  nfoprab2  7315  nfoprab3  7316  nfoprab  7317  nfmpo1  7333  nfmpo2  7334  nfmpo  7335  ovmpos  7399  ov2gf  7400  ov3  7413  nfof  7517  nfofr  7518  nftpos  8048  fvmpocurryd  8058  nffrecs  8070  nfwrecs  8103  nfwrecsOLD  8104  nfrecs  8177  nfrdg  8216  rdgsucmptf  8230  rdgsucmptnf  8231  frsucmpt  8239  frsucmptn  8240  nfixpw  8662  nfixp  8663  nfixp1  8664  xpcomco  8802  nfsup  9140  nfinf  9171  nfoi  9203  cnfcom3clem  9393  nfdju  9596  dfac8clem  9719  iunfo  10226  pwfseqlem2  10346  pwfseqlem4a  10348  pwfseqlem4  10349  reclem2pr  10735  nfseq  13659  nfwrd  14174  nfsum1  15329  nfsum  15330  nfsumOLD  15331  nfcprod1  15548  nfcprod  15549  symgval  18891  ptbasfi  22640  mbfsup  24733  itg1climres  24784  itg2splitlem  24818  itg2split  24819  nfitg1  24843  nfitg  24844  lgamgulm2  26090  lgseisenlem2  26429  lfgrnloop  27398  numclwlk2lem2f1o  28644  cnlnadjlem5  30334  2ndresdju  30887  nfesum1  31908  nfesum2  31909  ballotlem7  32402  bnj1230  32682  bnj1476  32727  bnj900  32809  bnj958  32820  bnj1000  32821  bnj1014  32841  bnj1123  32866  bnj1307  32903  bnj1321  32907  bnj1384  32912  bnj1398  32914  bnj1408  32916  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1447  32926  bnj1448  32927  bnj1449  32928  bnj1466  32933  bnj1467  32934  bnj1518  32944  bnj1519  32945  bnj1520  32946  bnj1525  32949  bnj1523  32951  cvmcov  33125  ttrclselem1  33711  ttrclselem2  33712  nfwsuc  33739  nfwlim  33743  nosupbnd2  33846  noinfbnd2  33861  nfaltop  34209  currysetlem1  35063  topdifinfindis  35444  rdgssun  35476  exrecfnlem  35477  finxpreclem6  35494  sdclem1  35828  riotasv2s  36899  cdleme26ee  38301  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32d  38385  cdleme32f  38387  cdleme40m  38408  cdleme40n  38409  ltrniotaval  38522  cdlemksv2  38788  cdlemkuv2  38808  cdlemk36  38854  cdlemk38  38856  cdlemkid  38877  cdlemk19x  38884  cdlemk11t  38887  areaquad  40963  nfscott  41746  nfcoll  41763  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  refsum2cnlem1  42469  eliuniincex  42548  disjrnmpt2  42615  fompt  42619  rnmptssbi  42696  allbutfi  42823  allbutfiinf  42850  fmuldfeqlem1  43013  fmuldfeq  43014  mullimc  43047  idlimc  43057  limcperiod  43059  neglimc  43078  addlimc  43079  0ellimcdiv  43080  fnlimcnv  43098  fnlimfvre  43105  fnlimfvre2  43108  fnlimf  43109  fnlimabslt  43110  xlimmnfmpt  43274  xlimpnfmpt  43275  cncfmptssg  43302  cncfshift  43305  cncficcgt0  43319  cncfiooicclem1  43324  dvnmul  43374  dvnprodlem1  43377  itgsinexplem1  43385  itgsubsticclem  43406  stoweidlem14  43445  stoweidlem16  43447  stoweidlem18  43449  stoweidlem22  43453  stoweidlem26  43457  stoweidlem27  43458  stoweidlem31  43462  stoweidlem32  43463  stoweidlem34  43465  stoweidlem35  43466  stoweidlem40  43471  stoweidlem41  43472  stoweidlem42  43473  stoweidlem44  43475  stoweidlem45  43476  stoweidlem46  43477  stoweidlem47  43478  stoweidlem48  43479  stoweidlem50  43481  stoweidlem51  43482  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  stoweidlem57  43488  stoweidlem59  43490  stoweidlem62  43493  wallispilem5  43500  stirlinglem4  43508  stirlinglem5  43509  stirlinglem8  43512  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  fourierdlem20  43558  fourierdlem31  43569  fourierdlem68  43605  fourierdlem80  43617  fourierdlem89  43626  fourierdlem91  43628  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem115  43652  fourierd  43653  fourierclimd  43654  etransclem48  43713  iundjiun  43888  meaiuninc3v  43912  ovnlerp  43990  ovncvrrp  43992  ovnhoilem1  44029  opnvonmbllem1  44060  iunhoiioolem  44103  vonioo  44110  vonicc  44113  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  issmff  44157  incsmflem  44164  smfconst  44172  decsmflem  44188  smfpreimagtf  44190  smflimlem2  44194  smflim  44199  smfpimgtxr  44202  smfresal  44209  smfmullem2  44213  smfmullem4  44215  smfpimbor1lem2  44220  smflim2  44226  smfpimcclem  44227  smflimmpt  44230  smfsup  44234  smfsupmpt  44235  smfsupxr  44236  smfinf  44238  smfinfmpt  44239  smflimsuplem2  44241  smflimsuplem5  44244  smflimsup  44248  smfliminf  44251  nfafv  44515  nfaov  44558  nfafv2  44597  prmdvdsfmtnof1lem1  44924  nfsetrecs  46278