Theorem nfcxfr 2922

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

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnfc 2909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-cleq 2754  df-clel 2837  df-nfc 2911

This theorem is used by:  nfrab1  3434  nfrabw  3450  nfrab  3451  nfsymdif  4206  nfpw  4579  nfpr  4656  nfsn  4671  nfop  4852  nfint  4920  nfiun  4986  nfiin  4987  nfiung  4988  nfiing  4989  nfii1  4991  nfopab1  5179  nfopab2  5180  nfmpt  5207  nfmpt1  5208  nfxp  5692  nfco  5849  nfcnv  5862  nfdm  5939  nfrn  5940  nfres  5978  nfima  6068  nfpred  6308  nfsuc  6436  nfiota1  6495  nffv  6892  fvmptss  7003  fvmptf  7012  fvopab5  7024  ralrnmptw  7090  ralrnmpt  7092  f1ompt  7107  fompt  7114  f1mpt  7261  fliftfun  7316  nfriota1  7380  riotaprop  7400  nfoprab1  7477  nfoprab2  7478  nfoprab3  7479  nfoprab  7480  nfmpo1  7496  nfmpo2  7497  nfmpo  7498  ovmpos  7564  ov2gf  7565  ov3  7579  nfof  7687  nfofr  7688  nftpos  8262  fvmpocurryd  8272  nffrecs  8285  nfwrecs  8316  nfrecs  8366  nfrdg  8406  rdgsucmptf  8420  rdgsucmptnf  8421  frsucmpt  8430  frsucmptn  8431  nfixpw  8926  nfixp  8927  nfixp1  8928  xpcomco  9068  nfsup  9424  nfinf  9456  nfoi  9489  cnfcom3clem  9687  ttrclselem1  9707  ttrclselem2  9708  nfscott  9874  nfdju  9915  dfac8clem  10038  iunfo  10550  pwfseqlem2  10671  pwfseqlem4a  10673  pwfseqlem4  10674  reclem2pr  11060  nfseq  14077  nfwrd  14610  nfsum1  15779  nfsum  15780  nfcprod1  15999  nfcprod  16000  symgval  19499  ptbasfi  23808  mbfsup  25893  itg1climres  25943  itg2splitlem  25977  itg2split  25978  nfitg1  26003  nfitg  26004  lgamgulm2  27270  lgseisenlem2  27610  nosupbnd2  27950  noinfbnd2  27965  nfseqs  28550  lfgrnloop  29568  numclwlk2lem2f1o  30845  cnlnadjlem5  32538  2ndresdju  33109  nfesum1  34537  nfesum2  34538  ballotlem7  35034  bnj1230  35298  bnj1476  35343  bnj900  35425  bnj958  35436  bnj1000  35437  bnj1014  35457  bnj1123  35482  bnj1307  35519  bnj1321  35523  bnj1384  35528  bnj1398  35530  bnj1408  35532  bnj1444  35539  bnj1445  35540  bnj1446  35541  bnj1447  35542  bnj1448  35543  bnj1449  35544  bnj1466  35549  bnj1467  35550  bnj1518  35560  bnj1519  35561  bnj1520  35562  bnj1525  35565  bnj1523  35567  cvmcov  35829  nfwsuc  36382  nfwlim  36386  nfaltop  36547  nfttc  37097  currysetlem1  37678  topdifinfindis  38087  rdgssun  38119  exrecfnlem  38120  finxpreclem6  38137  sdclem1  38480  riotasv2s  39818  cdleme26ee  41220  cdlemefs32sn1aw  41274  cdleme43fsv1snlem  41280  cdleme41sn3a  41293  cdleme32d  41304  cdleme32f  41306  cdleme40m  41327  cdleme40n  41328  ltrniotaval  41441  cdlemksv2  41707  cdlemkuv2  41727  cdlemk36  41773  cdlemk38  41775  cdlemkid  41796  cdlemk19x  41803  cdlemk11t  41806  areaquad  44044  nfcoll  45067  binomcxplemdvbinom  45164  binomcxplemdvsum  45166  binomcxplemnotnn0  45167  refsum2cnlem1  45858  eliuniincex  45928  disjrnmpt2  46007  rnmptssbi  46076  allbutfi  46209  allbutfiinf  46235  rexanuz2nf  46307  fmuldfeqlem1  46399  fmuldfeq  46400  mullimc  46433  idlimc  46443  limcperiod  46445  neglimc  46462  addlimc  46463  0ellimcdiv  46464  fnlimcnv  46482  fnlimfvre  46489  fnlimfvre2  46492  fnlimf  46493  fnlimabslt  46494  xlimmnfmpt  46658  xlimpnfmpt  46659  cncfmptssg  46686  cncfshift  46689  cncficcgt0  46703  cncfiooicclem1  46708  dvnmul  46758  dvnprodlem1  46761  itgsinexplem1  46769  itgsubsticclem  46790  stoweidlem14  46829  stoweidlem16  46831  stoweidlem18  46833  stoweidlem22  46837  stoweidlem26  46841  stoweidlem27  46842  stoweidlem31  46846  stoweidlem32  46847  stoweidlem34  46849  stoweidlem35  46850  stoweidlem40  46855  stoweidlem41  46856  stoweidlem42  46857  stoweidlem44  46859  stoweidlem45  46860  stoweidlem46  46861  stoweidlem47  46862  stoweidlem48  46863  stoweidlem50  46865  stoweidlem51  46866  stoweidlem52  46867  stoweidlem53  46868  stoweidlem54  46869  stoweidlem57  46872  stoweidlem59  46874  stoweidlem62  46877  wallispilem5  46884  stirlinglem4  46892  stirlinglem5  46893  stirlinglem8  46896  stirlinglem11  46899  stirlinglem12  46900  stirlinglem13  46901  stirlinglem14  46902  stirlinglem15  46903  fourierdlem20  46942  fourierdlem31  46953  fourierdlem68  46989  fourierdlem80  47001  fourierdlem89  47010  fourierdlem91  47012  fourierdlem103  47024  fourierdlem104  47025  fourierdlem112  47033  fourierdlem115  47036  fourierd  47037  fourierclimd  47038  etransclem48  47097  iundjiun  47275  meaiuninc3v  47299  ovnlerp  47377  ovncvrrp  47379  ovnhoilem1  47416  opnvonmbllem1  47447  iunhoiioolem  47490  vonioo  47497  vonicc  47500  pimdecfgtioc  47530  pimincfltioc  47531  pimdecfgtioo  47532  pimincfltioo  47533  issmff  47549  incsmflem  47556  smfpimltxr  47562  smfconst  47564  decsmflem  47581  smfpreimagtf  47583  smflimlem2  47587  smflim  47592  smfpimgtxr  47595  smfresal  47603  smfmullem2  47607  smfmullem4  47609  smfpimbor1lem2  47614  smflim2  47621  smfpimcclem  47622  smflimmpt  47625  smfsup  47629  smfsupmpt  47630  smfsupxr  47631  smfinf  47633  smfinfmpt  47634  smflimsuplem2  47636  smflimsuplem5  47639  smflimsup  47643  smfliminf  47646  smfpimne2  47655  smfdivdmmbl2  47656  fsupdm  47657  fsupdm2  47658  finfdm  47661  finfdm2  47662  nfafv  48011  nfaov  48054  nfafv2  48093  prmdvdsfmtnof1lem1  48474  nfsetrecs  50599