Theorem sselii 3600

Description: Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseli.1	|- A C_ B
sselii.2	|- C e. A

Assertion

Ref	Expression
sselii	|- C e. B

Proof of Theorem sselii

Step	Hyp	Ref	Expression
1		sselii.2	. 2 |- C e. A
2		sseli.1	. . 3 |- A C_ B
3	2	sseli 3599	. 2 |- ( C e. A -> C e. B )
4	1, 3	ax-mp 5	1 |- C e. B

Syntax hints:   e. wcel 1990   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseliALT  4791  fvrn0  6216  ovima0  6813  brtpos0  7359  wfrlem16  7430  rdg0  7517  iunfi  8254  rankdmr1  8664  rankeq0b  8723  cardprclem  8805  alephfp2  8932  dfac2  8953  sdom2en01  9124  fin56  9215  fin1a2lem10  9231  hsmexlem4  9251  canthp1lem2  9475  ax1cn  9970  recni  10052  0xr  10086  pnfxr  10092  nn0rei  11303  0xnn0  11369  nnzi  11401  nn0zi  11402  fprodge0  14724  lbsextlem4  19161  qsubdrg  19798  leordtval2  21016  iooordt  21021  hauspwdom  21304  comppfsc  21335  dfac14  21421  filconn  21687  isufil2  21712  iooretop  22569  ovolfiniun  23269  volfiniun  23315  iblabslem  23594  iblabs  23595  bddmulibl  23605  mdegcl  23829  logcn  24393  logccv  24409  leibpi  24669  xrlimcnp  24695  jensen  24715  emre  24732  lgsdir2lem3  25052  tgcgr4  25426  shelii  28072  chelii  28090  omlsilem  28261  nonbooli  28510  pjssmii  28540  riesz4  28923  riesz1  28924  cnlnadjeu  28937  nmopadjlei  28947  adjeq0  28950  dp2clq  29588  rpdp2cl  29589  dp2lt10  29591  dp2lt  29592  dp2ltc  29594  dplti  29613  qqh0  30028  qqh1  30029  qqhcn  30035  rrh0  30059  esumcst  30125  esumrnmpt2  30130  volmeas  30294  hgt750lem  30729  tgoldbachgtde  30738  kur14lem7  31194  kur14lem9  31196  iinllyconn  31236  bj-pinftyccb  33108  bj-minftyccb  33112  finixpnum  33394  poimirlem32  33441  ftc1cnnclem  33483  ftc2nc  33494  areacirclem2  33501  prdsbnd  33592  reheibor  33638  rmxyadd  37486  rmxy1  37487  rmxy0  37488  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  mpaaeu  37720  fourierdlem85  40408  fourierdlem102  40425  fourierdlem114  40437  iooborel  40569  hoicvrrex  40770