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

Theorem sselii 3980
Description: Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseli.1 𝐴𝐵
sselii.2 𝐶𝐴
Assertion
Ref Expression
sselii 𝐶𝐵

Proof of Theorem sselii
StepHypRef Expression
1 sselii.2 . 2 𝐶𝐴
2 sseli.1 . . 3 𝐴𝐵
32sseli 3979 . 2 (𝐶𝐴𝐶𝐵)
41, 3ax-mp 5 1 𝐶𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968
This theorem is referenced by:  sseliALT  5309  fvrn0  6936  ovima0  7612  brtpos0  8258  frrlem14  8324  wfrlem16OLD  8364  rdg0  8461  iunfi  9383  rankdmr1  9841  rankeq0b  9900  cardprclem  10019  alephfp2  10149  dfac2b  10171  sdom2en01  10342  fin56  10433  fin1a2lem10  10449  hsmexlem4  10469  canthp1lem2  10693  ax1cn  11189  recni  11275  0xr  11308  pnfxr  11315  nn0rei  12537  nn0cni  12538  0xnn0  12605  nnzi  12641  nn0zi  12642  seqexw  14058  mulgfval  19087  lbsextlem4  21163  qsubdrg  21437  leordtval2  23220  iooordt  23225  hauspwdom  23509  comppfsc  23540  dfac14  23626  filconn  23891  isufil2  23916  iooretop  24786  ovolfiniun  25536  volfiniun  25582  iblabslem  25863  iblabs  25864  bddmulibl  25874  mdegcl  26108  logcn  26689  logccv  26705  leibpi  26985  xrlimcnp  27011  jensen  27032  emre  27049  lgsdir2lem3  27371  shelii  31234  chelii  31252  omlsilem  31421  nonbooli  31670  pjssmii  31700  riesz4  32083  riesz1  32084  cnlnadjeu  32097  nmopadjlei  32107  adjeq0  32110  dp2clq  32863  rpdp2cl  32864  dp2lt10  32866  dp2lt  32867  dp2ltc  32869  dplti  32887  zringfrac  33582  qqh0  33985  qqh1  33986  qqhcn  33992  rrh0  34016  esumcst  34064  esumrnmpt2  34069  volmeas  34232  hgt750lem  34666  tgoldbachgtde  34675  kur14lem7  35217  kur14lem9  35219  iinllyconn  35259  bj-rdg0gALT  37072  bj-pinftyccb  37222  bj-minftyccb  37226  bj-rrdrg  37291  finixpnum  37612  poimirlem32  37659  ftc1cnnclem  37698  ftc2nc  37709  areacirclem2  37716  prdsbnd  37800  reheibor  37846  rmxyadd  42933  rmxy1  42934  rmxy0  42935  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  mpaaeu  43162  0iscard  43554  1iscard  43555  wfaxrep  45011  wfaxnul  45013  wfaxinf2  45018  fourierdlem85  46206  fourierdlem102  46223  fourierdlem114  46235  iooborel  46366  hoicvrrex  46571
  Copyright terms: Public domain W3C validator