Theorem sselii 3922

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 3921	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	ax-mp 5	1 ⊢ 𝐶 ∈ 𝐵

Syntax hints:   ∈ wcel 2109   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  sseliALT  5236  fvrn0  6796  ovima0  7442  brtpos0  8033  frrlem14  8099  wfrlem16OLD  8139  rdg0  8236  iunfi  9068  rankdmr1  9543  rankeq0b  9602  cardprclem  9721  alephfp2  9849  dfac2b  9870  sdom2en01  10042  fin56  10133  fin1a2lem10  10149  hsmexlem4  10169  canthp1lem2  10393  ax1cn  10889  recni  10973  0xr  11006  pnfxr  11013  nn0rei  12227  nn0cni  12228  0xnn0  12294  nnzi  12327  nn0zi  12328  seqexw  13718  mulgfval  18683  lbsextlem4  20404  qsubdrg  20631  leordtval2  22344  iooordt  22349  hauspwdom  22633  comppfsc  22664  dfac14  22750  filconn  23015  isufil2  23040  iooretop  23910  ovolfiniun  24646  volfiniun  24692  iblabslem  24973  iblabs  24974  bddmulibl  24984  mdegcl  25215  logcn  25783  logccv  25799  leibpi  26073  xrlimcnp  26099  jensen  26119  emre  26136  lgsdir2lem3  26456  shelii  29556  chelii  29574  omlsilem  29743  nonbooli  29992  pjssmii  30022  riesz4  30405  riesz1  30406  cnlnadjeu  30419  nmopadjlei  30429  adjeq0  30432  dp2clq  31134  rpdp2cl  31135  dp2lt10  31137  dp2lt  31138  dp2ltc  31140  dplti  31158  qqh0  31913  qqh1  31914  qqhcn  31920  rrh0  31944  esumcst  32010  esumrnmpt2  32015  volmeas  32178  hgt750lem  32610  tgoldbachgtde  32619  kur14lem7  33153  kur14lem9  33155  iinllyconn  33195  bj-rdg0gALT  35221  bj-pinftyccb  35371  bj-minftyccb  35375  bj-rrdrg  35440  finixpnum  35741  poimirlem32  35788  ftc1cnnclem  35827  ftc2nc  35838  areacirclem2  35845  prdsbnd  35930  reheibor  35976  rmxyadd  40723  rmxy1  40724  rmxy0  40725  rmydioph  40816  rmxdioph  40818  expdiophlem2  40824  expdioph  40825  mpaaeu  40955  fourierdlem85  43686  fourierdlem102  43703  fourierdlem114  43715  iooborel  43844  hoicvrrex  44048