Theorem sselii 3565

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

Step	Hyp	Ref	Expression
1		sselii.2	. 2 ⊢ 𝐶 ∈ 𝐴
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3564	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	ax-mp 5	1 ⊢ 𝐶 ∈ 𝐵

Syntax hints:   ∈ wcel 1977   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseliALT  4719  fvrn0  6126  ovima0  6711  brtpos0  7246  wfrlem16  7317  rdg0  7404  iunfi  8137  rankdmr1  8547  rankeq0b  8606  cardprclem  8688  alephfp2  8815  dfac2  8836  sdom2en01  9007  fin56  9098  fin1a2lem10  9114  hsmexlem4  9134  canthp1lem2  9354  ax1cn  9849  recni  9931  0xr  9965  pnfxr  9971  nn0rei  11180  0xnn0  11246  nnzi  11278  nn0zi  11279  fprodge0  14563  lbsextlem4  18982  qsubdrg  19617  leordtval2  20826  iooordt  20831  hauspwdom  21114  comppfsc  21145  dfac14  21231  filcon  21497  isufil2  21522  iooretop  22379  ovolfiniun  23076  volfiniun  23122  iblabslem  23400  iblabs  23401  bddmulibl  23411  mdegcl  23633  logcn  24193  logccv  24209  leibpi  24469  xrlimcnp  24495  jensen  24515  emre  24532  lgsdir2lem3  24852  tgcgr4  25226  shelii  27456  chelii  27474  omlsilem  27645  nonbooli  27894  pjssmii  27924  riesz4  28307  riesz1  28308  cnlnadjeu  28321  nmopadjlei  28331  adjeq0  28334  qqh0  29356  qqh1  29357  qqhcn  29363  rrh0  29387  esumcst  29452  esumrnmpt2  29457  volmeas  29621  kur14lem7  30448  kur14lem9  30450  iinllycon  30490  bj-pinftyccb  32285  bj-minftyccb  32289  finixpnum  32564  poimirlem32  32611  ftc1cnnclem  32653  ftc2nc  32664  areacirclem2  32671  prdsbnd  32762  reheibor  32808  rmxyadd  36504  rmxy1  36505  rmxy0  36506  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  mpaaeu  36739  fourierdlem85  39084  fourierdlem102  39101  fourierdlem114  39113  iooborel  39245  hoicvrrex  39446