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

Theorem sselii 3892
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 3891 . 2 (𝐶𝐴𝐶𝐵)
41, 3ax-mp 5 1 𝐶𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2083  wss 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880
This theorem is referenced by:  sseliALT  5111  fvrn0  6573  ovima0  7190  brtpos0  7757  wfrlem16  7829  rdg0  7916  iunfi  8665  rankdmr1  9083  rankeq0b  9142  cardprclem  9261  alephfp2  9388  dfac2b  9409  sdom2en01  9577  fin56  9668  fin1a2lem10  9684  hsmexlem4  9704  canthp1lem2  9928  ax1cn  10424  recni  10508  0xr  10541  pnfxr  10548  nn0rei  11762  nn0cni  11763  0xnn0  11827  nnzi  11860  nn0zi  11861  seqexw  13239  mulgfval  17987  lbsextlem4  19627  qsubdrg  20283  leordtval2  21508  iooordt  21513  hauspwdom  21797  comppfsc  21828  dfac14  21914  filconn  22179  isufil2  22204  iooretop  23061  ovolfiniun  23789  volfiniun  23835  iblabslem  24115  iblabs  24116  bddmulibl  24126  mdegcl  24350  logcn  24915  logccv  24931  leibpi  25206  xrlimcnp  25232  jensen  25252  emre  25269  lgsdir2lem3  25589  shelii  28679  chelii  28697  omlsilem  28866  nonbooli  29115  pjssmii  29145  riesz4  29528  riesz1  29529  cnlnadjeu  29542  nmopadjlei  29552  adjeq0  29555  dp2clq  30237  rpdp2cl  30238  dp2lt10  30240  dp2lt  30241  dp2ltc  30243  dplti  30261  qqh0  30838  qqh1  30839  qqhcn  30845  rrh0  30869  esumcst  30935  esumrnmpt2  30940  volmeas  31103  hgt750lem  31535  tgoldbachgtde  31544  kur14lem7  32069  kur14lem9  32071  iinllyconn  32111  frrlem14  32747  bj-pinftyccb  34082  bj-minftyccb  34086  finixpnum  34429  poimirlem32  34476  ftc1cnnclem  34517  ftc2nc  34528  areacirclem2  34535  prdsbnd  34624  reheibor  34670  rmxyadd  39024  rmxy1  39025  rmxy0  39026  rmydioph  39117  rmxdioph  39119  expdiophlem2  39125  expdioph  39126  mpaaeu  39256  fourierdlem85  42040  fourierdlem102  42057  fourierdlem114  42069  iooborel  42198  hoicvrrex  42402
  Copyright terms: Public domain W3C validator