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

Theorem sselii 3706
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 3705 . 2 (𝐶𝐴𝐶𝐵)
41, 3ax-mp 5 1 𝐶𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2103  wss 3680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-in 3687  df-ss 3694
This theorem is referenced by:  sseliALT  4899  fvrn0  6329  ovima0  6930  brtpos0  7479  wfrlem16  7550  rdg0  7637  iunfi  8370  rankdmr1  8777  rankeq0b  8836  cardprclem  8918  alephfp2  9045  dfac2  9066  sdom2en01  9237  fin56  9328  fin1a2lem10  9344  hsmexlem4  9364  canthp1lem2  9588  ax1cn  10083  recni  10165  0xr  10199  pnfxr  10205  nn0rei  11416  0xnn0  11482  nnzi  11514  nn0zi  11515  fprodge0  14844  lbsextlem4  19284  qsubdrg  19921  leordtval2  21139  iooordt  21144  hauspwdom  21427  comppfsc  21458  dfac14  21544  filconn  21809  isufil2  21834  iooretop  22691  ovolfiniun  23390  volfiniun  23436  iblabslem  23714  iblabs  23715  bddmulibl  23725  mdegcl  23949  logcn  24513  logccv  24529  leibpi  24789  xrlimcnp  24815  jensen  24835  emre  24852  lgsdir2lem3  25172  tgcgr4  25546  shelii  28302  chelii  28320  omlsilem  28491  nonbooli  28740  pjssmii  28770  riesz4  29153  riesz1  29154  cnlnadjeu  29167  nmopadjlei  29177  adjeq0  29180  dp2clq  29818  rpdp2cl  29819  dp2lt10  29821  dp2lt  29822  dp2ltc  29824  dplti  29843  qqh0  30258  qqh1  30259  qqhcn  30265  rrh0  30289  esumcst  30355  esumrnmpt2  30360  volmeas  30524  hgt750lem  30959  tgoldbachgtde  30968  kur14lem7  31422  kur14lem9  31424  iinllyconn  31464  bj-pinftyccb  33340  bj-minftyccb  33344  finixpnum  33626  poimirlem32  33673  ftc1cnnclem  33715  ftc2nc  33726  areacirclem2  33733  prdsbnd  33824  reheibor  33870  rmxyadd  37905  rmxy1  37906  rmxy0  37907  rmydioph  38000  rmxdioph  38002  expdiophlem2  38008  expdioph  38009  mpaaeu  38139  fourierdlem85  40828  fourierdlem102  40845  fourierdlem114  40857  iooborel  40989  hoicvrrex  41193
  Copyright terms: Public domain W3C validator