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

Theorem sselii 3915
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 3914 . 2 (𝐶𝐴𝐶𝐵)
41, 3ax-mp 5 1 𝐶𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  sseliALT  5180  fvrn0  6677  ovima0  7311  brtpos0  7886  wfrlem16  7957  rdg0  8044  iunfi  8800  rankdmr1  9218  rankeq0b  9277  cardprclem  9396  alephfp2  9524  dfac2b  9545  sdom2en01  9717  fin56  9808  fin1a2lem10  9824  hsmexlem4  9844  canthp1lem2  10068  ax1cn  10564  recni  10648  0xr  10681  pnfxr  10688  nn0rei  11900  nn0cni  11901  0xnn0  11965  nnzi  11998  nn0zi  11999  seqexw  13384  mulgfval  18221  lbsextlem4  19929  qsubdrg  20146  leordtval2  21820  iooordt  21825  hauspwdom  22109  comppfsc  22140  dfac14  22226  filconn  22491  isufil2  22516  iooretop  23374  ovolfiniun  24108  volfiniun  24154  iblabslem  24434  iblabs  24435  bddmulibl  24445  mdegcl  24673  logcn  25241  logccv  25257  leibpi  25531  xrlimcnp  25557  jensen  25577  emre  25594  lgsdir2lem3  25914  shelii  29001  chelii  29019  omlsilem  29188  nonbooli  29437  pjssmii  29467  riesz4  29850  riesz1  29851  cnlnadjeu  29864  nmopadjlei  29874  adjeq0  29877  dp2clq  30586  rpdp2cl  30587  dp2lt10  30589  dp2lt  30590  dp2ltc  30592  dplti  30610  qqh0  31333  qqh1  31334  qqhcn  31340  rrh0  31364  esumcst  31430  esumrnmpt2  31435  volmeas  31598  hgt750lem  32030  tgoldbachgtde  32039  kur14lem7  32567  kur14lem9  32569  iinllyconn  32609  frrlem14  33244  bj-pinftyccb  34631  bj-minftyccb  34635  bj-rrdrg  34699  finixpnum  35035  poimirlem32  35082  ftc1cnnclem  35121  ftc2nc  35132  areacirclem2  35139  prdsbnd  35224  reheibor  35270  rmxyadd  39849  rmxy1  39850  rmxy0  39851  rmydioph  39942  rmxdioph  39944  expdiophlem2  39950  expdioph  39951  mpaaeu  40081  fourierdlem85  42820  fourierdlem102  42837  fourierdlem114  42849  iooborel  42978  hoicvrrex  43182
  Copyright terms: Public domain W3C validator