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

Theorem sselii 3404
Description: Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseli.1  |-  A  C_  B
sselii.2  |-  C  e.  A
Assertion
Ref Expression
sselii  |-  C  e.  B

Proof of Theorem sselii
StepHypRef Expression
1 sselii.2 . 2  |-  C  e.  A
2 sseli.1 . . 3  |-  A  C_  B
32sseli 3403 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3ax-mp 5 1  |-  C  e.  B
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3386  df-ss 3393
This theorem is referenced by:  sseliALT  4500  fvrn0  5847  ovima0  6406  brtpos0  6935  wfrlem16  7006  rdg0  7094  iunfi  7815  rankdmr1  8224  rankeq0b  8283  cardprclem  8365  alephfp2  8491  dfac2  8512  sdom2en01  8683  fin56  8774  fin1a2lem10  8790  hsmexlem4  8810  canthp1lem2  9029  ax1cn  9524  recni  9606  0xr  9638  nn0rei  10831  nnzi  10912  nn0zi  10913  pnfxr  11363  ccatfnOLD  12666  fprodge0  13990  lbsextlem4  18327  qsubdrg  18963  leordtval2  20170  iooordt  20175  hauspwdom  20458  comppfsc  20489  dfac14  20575  filcon  20840  isufil2  20865  iooretop  21728  ovolfiniun  22396  volfiniun  22442  iblabslem  22727  iblabs  22728  bddmulibl  22738  mdegcl  22960  logcn  23534  logccv  23550  leibpi  23810  xrlimcnp  23836  jensen  23856  emre  23873  lgsdir2lem3  24195  tgcgr4  24518  shelii  26810  chelii  26828  omlsilem  26997  nonbooli  27246  pjssmii  27276  riesz4  27659  riesz1  27660  cnlnadjeu  27673  nmopadjlei  27683  adjeq0  27686  qqh0  28740  qqh1  28741  qqhcn  28747  rrh0  28771  esumcst  28836  esumrnmpt2  28841  volmeas  29006  kur14lem7  29887  kur14lem9  29889  iinllycon  29929  bj-pinftyccb  31570  bj-minftyccb  31574  finixpnum  31837  poimirlem32  31879  ftc1cnnclem  31922  ftc2nc  31933  areacirclem2  31940  prdsbnd  32032  reheibor  32078  rmxyadd  35682  rmxy1  35683  rmxy0  35684  rmydioph  35782  rmxdioph  35784  expdiophlem2  35790  expdioph  35791  mpaaeu  35929  fourierdlem85  37938  fourierdlem102  37955  fourierdlem114  37967  hoicvrrex  38225
  Copyright terms: Public domain W3C validator