MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elisset Unicode version

Theorem elisset 3120
Description: An element of a class exists. (Contributed by NM, 1-May-1995.)
Assertion
Ref Expression
elisset
Distinct variable group:   ,

Proof of Theorem elisset
StepHypRef Expression
1 elex 3118 . 2
2 isset 3113 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109
This theorem is referenced by:  elex2  3121  elex22  3122  ceqsalt  3132  ceqsalgALT  3135  cgsexg  3142  cgsex2g  3143  cgsex4g  3144  vtoclgft  3157  vtocleg  3180  vtoclegft  3181  spc2egv  3196  spc3egv  3198  tpid3g  4145  iinexg  4612  ralxfr2d  4668  copsex2t  4739  copsex2g  4740  fliftf  6213  eloprabga  6389  ovmpt4g  6425  eroveu  7425  mreiincl  14993  metustfbasOLD  21068  metustfbas  21069  spc2ed  27372  eqvincg  27374  elex2VD  33638  elex22VD  33639  tpid3gVD  33642  bnj852  33979  bnj938  33995  bnj1125  34048  bnj1148  34052  bnj1154  34055  bj-csbsnlem  34470  bj-snsetex  34521  bj-snglc  34527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator