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

Theorem sselii 3741
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 3740 . 2 (𝐶𝐴𝐶𝐵)
41, 3ax-mp 5 1 𝐶𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  sseliALT  4943  fvrn0  6377  ovima0  6978  brtpos0  7528  wfrlem16  7599  rdg0  7686  iunfi  8419  rankdmr1  8837  rankeq0b  8896  cardprclem  8995  alephfp2  9122  dfac2b  9143  dfac2OLD  9145  sdom2en01  9316  fin56  9407  fin1a2lem10  9423  hsmexlem4  9443  canthp1lem2  9667  ax1cn  10162  recni  10244  0xr  10278  pnfxr  10284  nn0rei  11495  0xnn0  11561  nnzi  11593  nn0zi  11594  fprodge0  14923  lbsextlem4  19363  qsubdrg  20000  leordtval2  21218  iooordt  21223  hauspwdom  21506  comppfsc  21537  dfac14  21623  filconn  21888  isufil2  21913  iooretop  22770  ovolfiniun  23469  volfiniun  23515  iblabslem  23793  iblabs  23794  bddmulibl  23804  mdegcl  24028  logcn  24592  logccv  24608  leibpi  24868  xrlimcnp  24894  jensen  24914  emre  24931  lgsdir2lem3  25251  tgcgr4  25625  shelii  28381  chelii  28399  omlsilem  28570  nonbooli  28819  pjssmii  28849  riesz4  29232  riesz1  29233  cnlnadjeu  29246  nmopadjlei  29256  adjeq0  29259  dp2clq  29897  rpdp2cl  29898  dp2lt10  29900  dp2lt  29901  dp2ltc  29903  dplti  29922  qqh0  30337  qqh1  30338  qqhcn  30344  rrh0  30368  esumcst  30434  esumrnmpt2  30439  volmeas  30603  hgt750lem  31038  tgoldbachgtde  31047  kur14lem7  31501  kur14lem9  31503  iinllyconn  31543  bj-pinftyccb  33419  bj-minftyccb  33423  finixpnum  33707  poimirlem32  33754  ftc1cnnclem  33796  ftc2nc  33807  areacirclem2  33814  prdsbnd  33905  reheibor  33951  rmxyadd  37988  rmxy1  37989  rmxy0  37990  rmydioph  38083  rmxdioph  38085  expdiophlem2  38091  expdioph  38092  mpaaeu  38222  fourierdlem85  40911  fourierdlem102  40928  fourierdlem114  40940  iooborel  41072  hoicvrrex  41276
  Copyright terms: Public domain W3C validator