Theorem sselii 3980

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ss 3968

This theorem is referenced by:  sseliALT  5309  fvrn0  6936  ovima0  7612  brtpos0  8258  frrlem14  8324  wfrlem16OLD  8364  rdg0  8461  iunfi  9383  rankdmr1  9841  rankeq0b  9900  cardprclem  10019  alephfp2  10149  dfac2b  10171  sdom2en01  10342  fin56  10433  fin1a2lem10  10449  hsmexlem4  10469  canthp1lem2  10693  ax1cn  11189  recni  11275  0xr  11308  pnfxr  11315  nn0rei  12537  nn0cni  12538  0xnn0  12605  nnzi  12641  nn0zi  12642  seqexw  14058  mulgfval  19087  lbsextlem4  21163  qsubdrg  21437  leordtval2  23220  iooordt  23225  hauspwdom  23509  comppfsc  23540  dfac14  23626  filconn  23891  isufil2  23916  iooretop  24786  ovolfiniun  25536  volfiniun  25582  iblabslem  25863  iblabs  25864  bddmulibl  25874  mdegcl  26108  logcn  26689  logccv  26705  leibpi  26985  xrlimcnp  27011  jensen  27032  emre  27049  lgsdir2lem3  27371  shelii  31234  chelii  31252  omlsilem  31421  nonbooli  31670  pjssmii  31700  riesz4  32083  riesz1  32084  cnlnadjeu  32097  nmopadjlei  32107  adjeq0  32110  dp2clq  32863  rpdp2cl  32864  dp2lt10  32866  dp2lt  32867  dp2ltc  32869  dplti  32887  zringfrac  33582  qqh0  33985  qqh1  33986  qqhcn  33992  rrh0  34016  esumcst  34064  esumrnmpt2  34069  volmeas  34232  hgt750lem  34666  tgoldbachgtde  34675  kur14lem7  35217  kur14lem9  35219  iinllyconn  35259  bj-rdg0gALT  37072  bj-pinftyccb  37222  bj-minftyccb  37226  bj-rrdrg  37291  finixpnum  37612  poimirlem32  37659  ftc1cnnclem  37698  ftc2nc  37709  areacirclem2  37716  prdsbnd  37800  reheibor  37846  rmxyadd  42933  rmxy1  42934  rmxy0  42935  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  mpaaeu  43162  0iscard  43554  1iscard  43555  wfaxrep  45011  wfaxnul  45013  wfaxinf2  45018  fourierdlem85  46206  fourierdlem102  46223  fourierdlem114  46235  iooborel  46366  hoicvrrex  46571