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 1570  Ⅎwnfc 2907

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 2732

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

This theorem is used by:  nfrab1  3431  nfrabw  3447  nfrab  3448  nfsymdif  4203  nfpw  4576  nfpr  4653  nfsn  4668  nfop  4849  nfint  4917  nfiun  4982  nfiin  4983  nfiung  4984  nfiing  4985  nfii1  4987  nfopab1  5175  nfopab2  5176  nfmpt  5203  nfmpt1  5204  nfxp  5681  nfco  5840  nfcnv  5853  nfdm  5930  nfrn  5931  nfres  5969  nfima  6059  nfpred  6299  nfsuc  6427  nfiota1  6486  nffv  6884  fvmptss  6995  fvmptf  7004  fvopab5  7016  ralrnmptw  7083  ralrnmpt  7085  f1ompt  7100  fompt  7107  f1mpt  7254  fliftfun  7309  nfriota1  7373  riotaprop  7393  nfoprab1  7470  nfoprab2  7471  nfoprab3  7472  nfoprab  7473  nfmpo1  7489  nfmpo2  7490  nfmpo  7491  ovmpos  7557  ov2gf  7558  ov3  7572  nfof  7683  nfofr  7684  nftpos  8257  fvmpocurryd  8267  nffrecs  8280  nfwrecs  8311  nfrecs  8361  nfrdg  8401  rdgsucmptf  8415  rdgsucmptnf  8416  frsucmpt  8425  frsucmptn  8426  nfixpw  8923  nfixp  8924  nfixp1  8925  xpcomco  9065  nfsup  9421  nfinf  9453  nfoi  9486  cnfcom3clem  9684  ttrclselem1  9704  ttrclselem2  9705  nfscott  9889  nfdju  9945  dfac8clem  10068  iunfo  10580  pwfseqlem2  10701  pwfseqlem4a  10703  pwfseqlem4  10704  reclem2pr  11090  nfseq  14108  nfwrd  14641  nfsum1  15810  nfsum  15811  nfcprod1  16030  nfcprod  16031  symgval  19532  ptbasfi  23847  mbfsup  25932  itg1climres  25982  itg2splitlem  26016  itg2split  26017  nfitg1  26041  nfitg  26042  lgamgulm2  27312  lgseisenlem2  27652  nosupbnd2  27992  noinfbnd2  28007  nfseqs  28592  lfgrnloop  29622  numclwlk2lem2f1o  30899  cnlnadjlem5  32592  2ndresdju  33162  nfesum1  34591  nfesum2  34592  ballotlem7  35088  bnj1230  35352  bnj1476  35397  bnj900  35479  bnj958  35490  bnj1000  35491  bnj1014  35511  bnj1123  35536  bnj1307  35573  bnj1321  35577  bnj1384  35582  bnj1398  35584  bnj1408  35586  bnj1444  35593  bnj1445  35594  bnj1446  35595  bnj1447  35596  bnj1448  35597  bnj1449  35598  bnj1466  35603  bnj1467  35604  bnj1518  35614  bnj1519  35615  bnj1520  35616  bnj1525  35619  bnj1523  35621  cvmcov  35943  nfwsuc  36496  nfwlim  36500  nfaltop  36661  nfttc  37195  currysetlem1  37776  topdifinfindis  38183  rdgssun  38215  exrecfnlem  38216  finxpreclem6  38233  sdclem1  38591  riotasv2s  39929  cdleme26ee  41331  cdlemefs32sn1aw  41385  cdleme43fsv1snlem  41391  cdleme41sn3a  41404  cdleme32d  41415  cdleme32f  41417  cdleme40m  41438  cdleme40n  41439  ltrniotaval  41552  cdlemksv2  41818  cdlemkuv2  41838  cdlemk36  41884  cdlemk38  41886  cdlemkid  41907  cdlemk19x  41914  cdlemk11t  41917  areaquad  44155  nfcoll  45178  binomcxplemdvbinom  45275  binomcxplemdvsum  45277  binomcxplemnotnn0  45278  refsum2cnlem1  45969  eliuniincex  46039  disjrnmpt2  46118  rnmptssbi  46187  allbutfi  46320  allbutfiinf  46346  rexanuz2nf  46418  fmuldfeqlem1  46510  fmuldfeq  46511  mullimc  46544  idlimc  46554  limcperiod  46556  neglimc  46573  addlimc  46574  0ellimcdiv  46575  fnlimcnv  46593  fnlimfvre  46600  fnlimfvre2  46603  fnlimf  46604  fnlimabslt  46605  xlimmnfmpt  46769  xlimpnfmpt  46770  cncfmptssg  46797  cncfshift  46800  cncficcgt0  46814  cncfiooicclem1  46819  dvnmul  46869  dvnprodlem1  46872  itgsinexplem1  46880  itgsubsticclem  46901  stoweidlem14  46940  stoweidlem16  46942  stoweidlem18  46944  stoweidlem22  46948  stoweidlem26  46952  stoweidlem27  46953  stoweidlem31  46957  stoweidlem32  46958  stoweidlem34  46960  stoweidlem35  46961  stoweidlem40  46966  stoweidlem41  46967  stoweidlem42  46968  stoweidlem44  46970  stoweidlem45  46971  stoweidlem46  46972  stoweidlem47  46973  stoweidlem48  46974  stoweidlem50  46976  stoweidlem51  46977  stoweidlem52  46978  stoweidlem53  46979  stoweidlem54  46980  stoweidlem57  46983  stoweidlem59  46985  stoweidlem62  46988  wallispilem5  46995  stirlinglem4  47003  stirlinglem5  47004  stirlinglem8  47007  stirlinglem11  47010  stirlinglem12  47011  stirlinglem13  47012  stirlinglem14  47013  stirlinglem15  47014  fourierdlem20  47053  fourierdlem31  47064  fourierdlem68  47100  fourierdlem80  47112  fourierdlem89  47121  fourierdlem91  47123  fourierdlem103  47135  fourierdlem104  47136  fourierdlem112  47144  fourierdlem115  47147  fourierd  47148  fourierclimd  47149  etransclem48  47208  iundjiun  47386  meaiuninc3v  47410  ovnlerp  47488  ovncvrrp  47490  ovnhoilem1  47527  opnvonmbllem1  47558  iunhoiioolem  47601  vonioo  47608  vonicc  47611  pimdecfgtioc  47641  pimincfltioc  47642  pimdecfgtioo  47643  pimincfltioo  47644  issmff  47660  incsmflem  47667  smfpimltxr  47673  smfconst  47675  decsmflem  47692  smfpreimagtf  47694  smflimlem2  47698  smflim  47703  smfpimgtxr  47706  smfresal  47714  smfmullem2  47718  smfmullem4  47720  smfpimbor1lem2  47725  smflim2  47732  smfpimcclem  47733  smflimmpt  47736  smfsup  47740  smfsupmpt  47741  smfsupxr  47742  smfinf  47744  smfinfmpt  47745  smflimsuplem2  47747  smflimsuplem5  47750  smflimsup  47754  smfliminf  47757  smfpimne2  47766  smfdivdmmbl2  47767  fsupdm  47768  fsupdm2  47769  finfdm  47772  finfdm2  47773  nfafv  48122  nfaov  48165  nfafv2  48204  prmdvdsfmtnof1lem1  48585  nfsetrecs  50705