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

Theorem sselii 3486
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 3485 . 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 1804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  sseliALT  4568  fvrn0  5878  ovima0  6439  brtpos0  6964  rdg0  7089  iunfi  7810  rankdmr1  8222  rankeq0b  8281  cardprclem  8363  alephfp2  8493  dfac2  8514  sdom2en01  8685  fin56  8776  fin1a2lem10  8792  hsmexlem4  8812  canthp1lem2  9034  ax1cn  9529  recni  9611  0xr  9643  nn0rei  10813  nnzi  10895  nn0zi  10896  pnfxr  11332  ccatfn  12573  lbsextlem4  17786  qsubdrg  18449  leordtval2  19691  iooordt  19696  hauspwdom  19980  comppfsc  20011  dfac14  20097  filcon  20362  isufil2  20387  iooretop  21251  ovolfiniun  21890  volfiniun  21935  iblabslem  22212  iblabs  22213  bddmulibl  22223  mdegcl  22447  logcn  23006  logccv  23022  leibpi  23251  xrlimcnp  23276  jensen  23296  emre  23313  lgsdir2lem3  23578  shelii  26110  chelii  26129  omlsilem  26298  nonbooli  26547  pjssmii  26577  riesz4  26961  riesz1  26962  cnlnadjeu  26975  nmopadjlei  26985  adjeq0  26988  qqh0  27943  qqh1  27944  qqhcn  27950  esumcst  28049  volmeas  28181  kur14lem7  28634  kur14lem9  28636  iinllycon  28677  wfrlem16  29334  finixpnum  30014  ftc1cnnclem  30064  ftc2nc  30075  areacirclem2  30084  prdsbnd  30265  reheibor  30311  rmxyadd  30833  rmxy1  30834  rmxy0  30835  rmydioph  30932  rmxdioph  30934  expdiophlem2  30940  expdioph  30941  mpaaeu  31075  fprodge0  31551  fourierdlem85  31928  fourierdlem102  31945  fourierdlem114  31957  bj-pinftyccb  34499  bj-minftyccb  34503
  Copyright terms: Public domain W3C validator