Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcxfr Structured version   Visualization version   GIF version

Theorem nfcxfr 2953
 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
StepHypRef Expression
1 nfcxfr.2 . 2 𝑥𝐵
2 nfcxfr.1 . . 3 𝐴 = 𝐵
32nfceqi 2952 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 234 1 𝑥𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  Ⅎwnfc 2936 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870  df-nfc 2938 This theorem is referenced by:  nfrab1  3338  nfrabw  3339  nfrab  3340  nfdif  4056  nfun  4095  nfin  4146  nfsymdif  4176  nfpw  4521  nfpr  4591  nfsn  4606  nfop  4785  nfint  4852  nfiun  4915  nfiin  4916  nfiung  4917  nfiing  4918  nfiu1  4919  nfii1  4920  nfopab  5102  nfopab1  5103  nfopab2  5104  nfmpt  5131  nfmpt1  5132  nfxp  5556  nfco  5704  nfcnv  5717  nfdm  5791  nfrn  5792  nfres  5824  nfima  5908  nfpred  6128  nfsuc  6237  nfiota1  6293  nffv  6665  fvmptss  6767  fvmptf  6776  fvopab5  6787  ralrnmptw  6847  ralrnmpt  6849  f1ompt  6862  f1mpt  7007  fliftfun  7054  nfriota1  7110  riotaprop  7130  nfoprab1  7204  nfoprab2  7205  nfoprab3  7206  nfoprab  7207  nfmpo1  7223  nfmpo2  7224  nfmpo  7225  ovmpos  7288  ov2gf  7289  ov3  7302  nfof  7405  nfofr  7406  nftpos  7928  fvmpocurryd  7938  nfwrecs  7950  nfrecs  8012  nfrdg  8051  rdgsucmptf  8065  rdgsucmptnf  8066  frsucmpt  8074  frsucmptn  8075  nfixpw  8481  nfixp  8482  nfixp1  8483  xpcomco  8608  nfsup  8917  nfinf  8948  nfoi  8980  cnfcom3clem  9170  nfdju  9338  dfac8clem  9461  iunfo  9968  pwfseqlem2  10088  pwfseqlem4a  10090  pwfseqlem4  10091  reclem2pr  10477  nfseq  13394  nfwrd  13906  nfsum1  15058  nfsum  15059  nfsumOLD  15060  nfcprod1  15276  nfcprod  15277  symgval  18510  ptbasfi  22227  mbfsup  24309  itg1climres  24359  itg2splitlem  24393  itg2split  24394  nfitg1  24418  nfitg  24419  lgamgulm2  25665  lgseisenlem2  26004  lfgrnloop  26962  numclwlk2lem2f1o  28208  cnlnadjlem5  29898  2ndresdju  30455  nfesum1  31475  nfesum2  31476  ballotlem7  31969  bnj1230  32250  bnj1476  32295  bnj900  32377  bnj958  32388  bnj1000  32389  bnj1014  32409  bnj1123  32434  bnj1307  32471  bnj1321  32475  bnj1384  32480  bnj1398  32482  bnj1408  32484  bnj1444  32491  bnj1445  32492  bnj1446  32493  bnj1447  32494  bnj1448  32495  bnj1449  32496  bnj1466  32501  bnj1467  32502  bnj1518  32512  bnj1519  32513  bnj1520  32514  bnj1525  32517  bnj1523  32519  cvmcov  32689  nfwsuc  33288  nfwlim  33292  nffrecs  33303  nosupbnd2  33406  noinfbnd2  33421  nfaltop  33701  currysetlem1  34533  topdifinfindis  34914  rdgssun  34946  exrecfnlem  34947  finxpreclem6  34964  sdclem1  35332  riotasv2s  36405  cdleme26ee  37807  cdlemefs32sn1aw  37861  cdleme43fsv1snlem  37867  cdleme41sn3a  37880  cdleme32d  37891  cdleme32f  37893  cdleme40m  37914  cdleme40n  37915  ltrniotaval  38028  cdlemksv2  38294  cdlemkuv2  38314  cdlemk36  38360  cdlemk38  38362  cdlemkid  38383  cdlemk19x  38390  cdlemk11t  38393  areaquad  40337  nfscott  41118  nfcoll  41135  binomcxplemdvbinom  41228  binomcxplemdvsum  41230  binomcxplemnotnn0  41231  refsum2cnlem1  41837  eliuniincex  41916  suprnmpt  41969  disjrnmpt2  41985  fompt  41989  rnmptssbi  42067  allbutfi  42197  allbutfiinf  42225  fmuldfeqlem1  42392  fmuldfeq  42393  mullimc  42426  idlimc  42436  limcperiod  42438  neglimc  42457  addlimc  42458  0ellimcdiv  42459  fnlimcnv  42477  fnlimfvre  42484  fnlimfvre2  42487  fnlimf  42488  fnlimabslt  42489  xlimmnfmpt  42653  xlimpnfmpt  42654  cncfmptssg  42681  cncfshift  42684  cncficcgt0  42698  cncfiooicclem1  42703  dvnmul  42753  dvnprodlem1  42756  itgsinexplem1  42764  itgsubsticclem  42785  stoweidlem14  42824  stoweidlem16  42826  stoweidlem18  42828  stoweidlem22  42832  stoweidlem26  42836  stoweidlem27  42837  stoweidlem31  42841  stoweidlem32  42842  stoweidlem34  42844  stoweidlem35  42845  stoweidlem40  42850  stoweidlem41  42851  stoweidlem42  42852  stoweidlem44  42854  stoweidlem45  42855  stoweidlem46  42856  stoweidlem47  42857  stoweidlem48  42858  stoweidlem50  42860  stoweidlem51  42861  stoweidlem52  42862  stoweidlem53  42863  stoweidlem54  42864  stoweidlem57  42867  stoweidlem59  42869  stoweidlem62  42872  wallispilem5  42879  stirlinglem4  42887  stirlinglem5  42888  stirlinglem8  42891  stirlinglem11  42894  stirlinglem12  42895  stirlinglem13  42896  stirlinglem14  42897  stirlinglem15  42898  fourierdlem20  42937  fourierdlem31  42948  fourierdlem68  42984  fourierdlem80  42996  fourierdlem89  43005  fourierdlem91  43007  fourierdlem103  43019  fourierdlem104  43020  fourierdlem112  43028  fourierdlem115  43031  fourierd  43032  fourierclimd  43033  etransclem48  43092  iundjiun  43267  meaiuninc3v  43291  ovnlerp  43369  ovncvrrp  43371  ovnhoilem1  43408  opnvonmbllem1  43439  iunhoiioolem  43482  vonioo  43489  vonicc  43492  pimdecfgtioc  43518  pimincfltioc  43519  pimdecfgtioo  43520  pimincfltioo  43521  issmff  43536  incsmflem  43543  smfconst  43551  decsmflem  43567  smfpreimagtf  43569  smflimlem2  43573  smflim  43578  smfpimgtxr  43581  smfresal  43588  smfmullem2  43592  smfmullem4  43594  smfpimbor1lem2  43599  smflim2  43605  smfpimcclem  43606  smflimmpt  43609  smfsup  43613  smfsupmpt  43614  smfsupxr  43615  smfinf  43617  smfinfmpt  43618  smflimsuplem2  43620  smflimsuplem5  43623  smflimsup  43627  smfliminf  43630  nfafv  43860  nfaov  43903  nfafv2  43942  prmdvdsfmtnof1lem1  44269  nfsetrecs  45382
 Copyright terms: Public domain W3C validator