Theorem nfcxfr 2920

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

This proof depends on syntax axioms:   = wceq 1569  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  nfrab1  3431  nfrabw  3447  nfrab  3448  nfsymdif  4202  nfpw  4575  nfpr  4652  nfsn  4667  nfop  4848  nfint  4916  nfiun  4981  nfiin  4982  nfiung  4983  nfiing  4984  nfii1  4986  nfopab1  5174  nfopab2  5175  nfmpt  5202  nfmpt1  5203  nfxp  5683  nfco  5842  nfcnv  5855  nfdm  5932  nfrn  5933  nfres  5971  nfima  6063  nfpred  6309  nfsuc  6437  nfiota1  6496  nffv  6895  fvmptss  7006  fvmptf  7015  fvopab5  7027  ralrnmptw  7094  ralrnmpt  7096  f1ompt  7111  fompt  7118  f1mpt  7265  fliftfun  7320  nfriota1  7384  riotaprop  7404  nfoprab1  7481  nfoprab2  7482  nfoprab3  7483  nfoprab  7484  nfmpo1  7500  nfmpo2  7501  nfmpo  7502  ovmpos  7568  ov2gf  7569  ov3  7583  nfof  7699  nfofr  7700  nftpos  8278  fvmpocurryd  8288  nffrecs  8301  nfwrecs  8332  nfrecs  8382  nfrdg  8422  rdgsucmptf  8436  rdgsucmptnf  8437  frsucmpt  8446  frsucmptn  8447  nfixpw  8944  nfixp  8945  nfixp1  8946  xpcomco  9086  nfsup  9443  nfinf  9475  nfoi  9508  cnfcom3clem  9706  ttrclselem1  9726  ttrclselem2  9727  nfscott  9932  nfdju  9988  dfac8clem  10111  iunfo  10623  pwfseqlem2  10744  pwfseqlem4a  10746  pwfseqlem4  10747  reclem2pr  11133  nfseq  14154  nfwrd  14688  nfsum1  15857  nfsum  15858  nfcprod1  16077  nfcprod  16078  symgval  19585  ptbasfi  23900  mbfsup  25985  itg1climres  26035  itg2splitlem  26069  itg2split  26070  nfitg1  26094  nfitg  26095  lgamgulm2  27363  lgseisenlem2  27703  nosupbnd2  28073  noinfbnd2  28088  nfseqs  28673  lfgrnloop  29703  numclwlk2lem2f1o  30980  cnlnadjlem5  32673  2ndresdju  33243  nfesum1  34672  nfesum2  34673  ballotlem7  35168  bnj1230  35432  bnj1476  35477  bnj900  35559  bnj958  35570  bnj1000  35571  bnj1014  35591  bnj1123  35616  bnj1307  35653  bnj1321  35657  bnj1384  35662  bnj1398  35664  bnj1408  35666  bnj1444  35673  bnj1445  35674  bnj1446  35675  bnj1447  35676  bnj1448  35677  bnj1449  35678  bnj1466  35683  bnj1467  35684  bnj1518  35694  bnj1519  35695  bnj1520  35696  bnj1525  35699  bnj1523  35701  onprcf1acwevdlem2  35896  cvmcov  36028  nfwsuc  36580  nfwlim  36584  nfaltop  36745  nfttc  37279  currysetlem1  37860  topdifinfindis  38270  rdgssun  38302  exrecfnlem  38303  finxpreclem6  38320  sdclem1  38678  riotasv2s  40016  cdleme26ee  41418  cdlemefs32sn1aw  41472  cdleme43fsv1snlem  41478  cdleme41sn3a  41491  cdleme32d  41502  cdleme32f  41504  cdleme40m  41525  cdleme40n  41526  ltrniotaval  41639  cdlemksv2  41905  cdlemkuv2  41925  cdlemk36  41971  cdlemk38  41973  cdlemkid  41994  cdlemk19x  42001  cdlemk11t  42004  areaquad  44218  nfcoll  45240  binomcxplemdvbinom  45337  binomcxplemdvsum  45339  binomcxplemnotnn0  45340  refsum2cnlem1  46054  eliuniincex  46124  disjrnmpt2  46203  rnmptssbi  46272  allbutfi  46404  allbutfiinf  46430  rexanuz2nf  46502  fmuldfeqlem1  46594  fmuldfeq  46595  mullimc  46628  idlimc  46638  limcperiod  46640  neglimc  46657  addlimc  46658  0ellimcdiv  46659  fnlimcnv  46677  fnlimfvre  46684  fnlimfvre2  46687  fnlimf  46688  fnlimabslt  46689  xlimmnfmpt  46853  xlimpnfmpt  46854  cncfmptssg  46881  cncfshift  46884  cncficcgt0  46898  cncfiooicclem1  46903  dvnmul  46953  dvnprodlem1  46956  itgsinexplem1  46964  itgsubsticclem  46985  stoweidlem14  47024  stoweidlem16  47026  stoweidlem18  47028  stoweidlem22  47032  stoweidlem26  47036  stoweidlem27  47037  stoweidlem31  47041  stoweidlem32  47042  stoweidlem34  47044  stoweidlem35  47045  stoweidlem40  47050  stoweidlem41  47051  stoweidlem42  47052  stoweidlem44  47054  stoweidlem45  47055  stoweidlem46  47056  stoweidlem47  47057  stoweidlem48  47058  stoweidlem50  47060  stoweidlem51  47061  stoweidlem52  47062  stoweidlem53  47063  stoweidlem54  47064  stoweidlem57  47067  stoweidlem59  47069  stoweidlem62  47072  wallispilem5  47079  stirlinglem4  47087  stirlinglem5  47088  stirlinglem8  47091  stirlinglem11  47094  stirlinglem12  47095  stirlinglem13  47096  stirlinglem14  47097  stirlinglem15  47098  fourierdlem20  47137  fourierdlem31  47148  fourierdlem68  47184  fourierdlem80  47196  fourierdlem89  47205  fourierdlem91  47207  fourierdlem103  47219  fourierdlem104  47220  fourierdlem112  47228  fourierdlem115  47231  fourierd  47232  fourierclimd  47233  etransclem48  47292  iundjiun  47470  meaiuninc3v  47494  ovnlerp  47572  ovncvrrp  47574  ovnhoilem1  47611  opnvonmbllem1  47642  iunhoiioolem  47685  vonioo  47692  vonicc  47695  pimdecfgtioc  47725  pimincfltioc  47726  pimdecfgtioo  47727  pimincfltioo  47728  issmff  47744  incsmflem  47751  smfpimltxr  47757  smfconst  47759  decsmflem  47776  smfpreimagtf  47778  smflimlem2  47782  smflim  47787  smfpimgtxr  47790  smfresal  47798  smfmullem2  47802  smfmullem4  47804  smfpimbor1lem2  47809  smflim2  47816  smfpimcclem  47817  smflimmpt  47820  smfsup  47824  smfsupmpt  47825  smfsupxr  47826  smfinf  47828  smfinfmpt  47829  smflimsuplem2  47831  smflimsuplem5  47834  smflimsup  47838  smfliminf  47841  smfpimne2  47850  smfdivdmmbl2  47851  fsupdm  47852  fsupdm2  47853  finfdm  47856  finfdm2  47857  nfafv  48206  nfaov  48249  nfafv2  48288  prmdvdsfmtnof1lem1  48669  nfsetrecs  50789