Theorem nfcxfr 2929

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

Syntax hints:   = wceq 1567  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-cleq 2761  df-clel 2844  df-nfc 2918

This theorem is referenced by:  nfrab1  3442  nfrabw  3458  nfrab  3459  nfsymdif  4216  nfpw  4584  nfpr  4661  nfsn  4676  nfop  4856  nfint  4924  nfiun  4990  nfiin  4991  nfiung  4992  nfiing  4993  nfii1  4995  nfopab1  5183  nfopab2  5184  nfmpt  5211  nfmpt1  5212  nfxp  5695  nfco  5852  nfcnv  5865  nfdm  5942  nfrn  5943  nfres  5981  nfima  6071  nfpred  6308  nfsuc  6436  nfiota1  6495  nffv  6892  fvmptss  7003  fvmptf  7012  fvopab5  7024  ralrnmptw  7090  ralrnmpt  7092  f1ompt  7107  fompt  7114  f1mpt  7260  fliftfun  7311  nfriota1  7375  riotaprop  7395  nfoprab1  7472  nfoprab2  7473  nfoprab3  7474  nfoprab  7475  nfmpo1  7491  nfmpo2  7492  nfmpo  7493  ovmpos  7559  ov2gf  7560  ov3  7574  nfof  7681  nfofr  7682  nftpos  8257  fvmpocurryd  8267  nffrecs  8280  nfwrecs  8311  nfrecs  8361  nfrdg  8401  rdgsucmptf  8415  rdgsucmptnf  8416  frsucmpt  8425  frsucmptn  8426  nfixpw  8914  nfixp  8915  nfixp1  8916  xpcomco  9055  nfsup  9411  nfinf  9443  nfoi  9476  cnfcom3clem  9674  ttrclselem1  9694  ttrclselem2  9695  nfscott  9865  nfdju  9893  dfac8clem  10016  iunfo  10523  pwfseqlem2  10644  pwfseqlem4a  10646  pwfseqlem4  10647  reclem2pr  11033  nfseq  14047  nfwrd  14580  nfsum1  15741  nfsum  15742  nfcprod1  15962  nfcprod  15963  symgval  19441  ptbasfi  23707  mbfsup  25792  itg1climres  25842  itg2splitlem  25876  itg2split  25877  nfitg1  25902  nfitg  25903  lgamgulm2  27166  lgseisenlem2  27506  nosupbnd2  27846  noinfbnd2  27861  nfseqs  28446  lfgrnloop  29416  numclwlk2lem2f1o  30671  cnlnadjlem5  32364  2ndresdju  32935  nfesum1  34375  nfesum2  34376  ballotlem7  34871  bnj1230  35135  bnj1476  35180  bnj900  35262  bnj958  35273  bnj1000  35274  bnj1014  35294  bnj1123  35319  bnj1307  35356  bnj1321  35360  bnj1384  35365  bnj1398  35367  bnj1408  35369  bnj1444  35376  bnj1445  35377  bnj1446  35378  bnj1447  35379  bnj1448  35380  bnj1449  35381  bnj1466  35386  bnj1467  35387  bnj1518  35397  bnj1519  35398  bnj1520  35399  bnj1525  35402  bnj1523  35404  cvmcov  35688  nfwsuc  36241  nfwlim  36245  nfaltop  36405  nfttc  36925  currysetlem1  37506  topdifinfindis  37915  rdgssun  37947  exrecfnlem  37948  finxpreclem6  37965  sdclem1  38317  riotasv2s  39657  cdleme26ee  41059  cdlemefs32sn1aw  41113  cdleme43fsv1snlem  41119  cdleme41sn3a  41132  cdleme32d  41143  cdleme32f  41145  cdleme40m  41166  cdleme40n  41167  ltrniotaval  41280  cdlemksv2  41546  cdlemkuv2  41566  cdlemk36  41612  cdlemk38  41614  cdlemkid  41635  cdlemk19x  41642  cdlemk11t  41645  areaquad  43870  nfcoll  44893  binomcxplemdvbinom  44990  binomcxplemdvsum  44992  binomcxplemnotnn0  44993  refsum2cnlem1  45684  eliuniincex  45754  disjrnmpt2  45833  rnmptssbi  45902  allbutfi  46035  allbutfiinf  46061  rexanuz2nf  46133  fmuldfeqlem1  46225  fmuldfeq  46226  mullimc  46259  idlimc  46269  limcperiod  46271  neglimc  46288  addlimc  46289  0ellimcdiv  46290  fnlimcnv  46308  fnlimfvre  46315  fnlimfvre2  46318  fnlimf  46319  fnlimabslt  46320  xlimmnfmpt  46484  xlimpnfmpt  46485  cncfmptssg  46512  cncfshift  46515  cncficcgt0  46529  cncfiooicclem1  46534  dvnmul  46584  dvnprodlem1  46587  itgsinexplem1  46595  itgsubsticclem  46616  stoweidlem14  46655  stoweidlem16  46657  stoweidlem18  46659  stoweidlem22  46663  stoweidlem26  46667  stoweidlem27  46668  stoweidlem31  46672  stoweidlem32  46673  stoweidlem34  46675  stoweidlem35  46676  stoweidlem40  46681  stoweidlem41  46682  stoweidlem42  46683  stoweidlem44  46685  stoweidlem45  46686  stoweidlem46  46687  stoweidlem47  46688  stoweidlem48  46689  stoweidlem50  46691  stoweidlem51  46692  stoweidlem52  46693  stoweidlem53  46694  stoweidlem54  46695  stoweidlem57  46698  stoweidlem59  46700  stoweidlem62  46703  wallispilem5  46710  stirlinglem4  46718  stirlinglem5  46719  stirlinglem8  46722  stirlinglem11  46725  stirlinglem12  46726  stirlinglem13  46727  stirlinglem14  46728  stirlinglem15  46729  fourierdlem20  46768  fourierdlem31  46779  fourierdlem68  46815  fourierdlem80  46827  fourierdlem89  46836  fourierdlem91  46838  fourierdlem103  46850  fourierdlem104  46851  fourierdlem112  46859  fourierdlem115  46862  fourierd  46863  fourierclimd  46864  etransclem48  46923  iundjiun  47101  meaiuninc3v  47125  ovnlerp  47203  ovncvrrp  47205  ovnhoilem1  47242  opnvonmbllem1  47273  iunhoiioolem  47316  vonioo  47323  vonicc  47326  pimdecfgtioc  47356  pimincfltioc  47357  pimdecfgtioo  47358  pimincfltioo  47359  issmff  47375  incsmflem  47382  smfpimltxr  47388  smfconst  47390  decsmflem  47407  smfpreimagtf  47409  smflimlem2  47413  smflim  47418  smfpimgtxr  47421  smfresal  47429  smfmullem2  47433  smfmullem4  47435  smfpimbor1lem2  47440  smflim2  47447  smfpimcclem  47448  smflimmpt  47451  smfsup  47455  smfsupmpt  47456  smfsupxr  47457  smfinf  47459  smfinfmpt  47460  smflimsuplem2  47462  smflimsuplem5  47465  smflimsup  47469  smfliminf  47472  smfpimne2  47481  smfdivdmmbl2  47482  fsupdm  47483  fsupdm2  47484  finfdm  47487  finfdm2  47488  nfafv  47797  nfaov  47840  nfafv2  47879  prmdvdsfmtnof1lem1  48260  nfsetrecs  50384