Theorem sselii 3991

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

Syntax hints:   ∈ wcel 2105   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979

This theorem is referenced by:  sseliALT  5314  fvrn0  6936  ovima0  7611  brtpos0  8256  frrlem14  8322  wfrlem16OLD  8362  rdg0  8459  iunfi  9380  rankdmr1  9838  rankeq0b  9897  cardprclem  10016  alephfp2  10146  dfac2b  10168  sdom2en01  10339  fin56  10430  fin1a2lem10  10446  hsmexlem4  10466  canthp1lem2  10690  ax1cn  11186  recni  11272  0xr  11305  pnfxr  11312  nn0rei  12534  nn0cni  12535  0xnn0  12602  nnzi  12638  nn0zi  12639  seqexw  14054  mulgfval  19099  lbsextlem4  21180  qsubdrg  21454  leordtval2  23235  iooordt  23240  hauspwdom  23524  comppfsc  23555  dfac14  23641  filconn  23906  isufil2  23931  iooretop  24801  ovolfiniun  25549  volfiniun  25595  iblabslem  25877  iblabs  25878  bddmulibl  25888  mdegcl  26122  logcn  26703  logccv  26719  leibpi  26999  xrlimcnp  27025  jensen  27046  emre  27063  lgsdir2lem3  27385  shelii  31243  chelii  31261  omlsilem  31430  nonbooli  31679  pjssmii  31709  riesz4  32092  riesz1  32093  cnlnadjeu  32106  nmopadjlei  32116  adjeq0  32119  dp2clq  32847  rpdp2cl  32848  dp2lt10  32850  dp2lt  32851  dp2ltc  32853  dplti  32871  zringfrac  33561  qqh0  33946  qqh1  33947  qqhcn  33953  rrh0  33977  esumcst  34043  esumrnmpt2  34048  volmeas  34211  hgt750lem  34644  tgoldbachgtde  34653  kur14lem7  35196  kur14lem9  35198  iinllyconn  35238  bj-rdg0gALT  37053  bj-pinftyccb  37203  bj-minftyccb  37207  bj-rrdrg  37272  finixpnum  37591  poimirlem32  37638  ftc1cnnclem  37677  ftc2nc  37688  areacirclem2  37695  prdsbnd  37779  reheibor  37825  rmxyadd  42909  rmxy1  42910  rmxy0  42911  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  mpaaeu  43138  0iscard  43530  1iscard  43531  wfaxrep  44949  fourierdlem85  46146  fourierdlem102  46163  fourierdlem114  46175  iooborel  46306  hoicvrrex  46511