Theorem sselii 3919

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907

This theorem is referenced by:  sseliALT  5244  fvrn0  6862  ovima0  7539  brtpos0  8176  frrlem14  8242  rdg0  8353  iunfi  9246  rankdmr1  9716  rankeq0b  9775  cardprclem  9894  alephfp2  10022  dfac2b  10044  sdom2en01  10215  fin56  10306  fin1a2lem10  10322  hsmexlem4  10342  canthp1lem2  10567  ax1cn  11063  recni  11150  0xr  11183  pnfxr  11190  nn0rei  12439  nn0cni  12440  0xnn0  12507  nnzi  12542  nn0zi  12543  seqexw  13970  mulgfval  19036  lbsextlem4  21151  qsubdrg  21409  leordtval2  23187  iooordt  23192  hauspwdom  23476  comppfsc  23507  dfac14  23593  filconn  23858  isufil2  23883  iooretop  24740  ovolfiniun  25478  volfiniun  25524  iblabslem  25805  iblabs  25806  bddmulibl  25816  mdegcl  26044  logcn  26624  logccv  26640  leibpi  26919  xrlimcnp  26945  jensen  26966  emre  26983  lgsdir2lem3  27304  shelii  31301  chelii  31319  omlsilem  31488  nonbooli  31737  pjssmii  31767  riesz4  32150  riesz1  32151  cnlnadjeu  32164  nmopadjlei  32174  adjeq0  32177  dp2clq  32955  rpdp2cl  32956  dp2lt10  32958  dp2lt  32959  dp2ltc  32961  dplti  32979  zringfrac  33629  vieta  33739  qqh0  34144  qqh1  34145  qqhcn  34151  rrh0  34175  esumcst  34223  esumrnmpt2  34228  volmeas  34391  hgt750lem  34811  tgoldbachgtde  34820  kur14lem7  35410  kur14lem9  35412  iinllyconn  35452  bj-rdg0gALT  37394  bj-pinftyccb  37551  bj-minftyccb  37555  bj-rrdrg  37620  finixpnum  37940  poimirlem32  37987  ftc1cnnclem  38026  ftc2nc  38037  areacirclem2  38044  prdsbnd  38128  reheibor  38174  rmxyadd  43367  rmxy1  43368  rmxy0  43369  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  mpaaeu  43596  0iscard  43986  1iscard  43987  wfaxrep  45439  wfaxnul  45441  wfaxinf2  45446  fourierdlem85  46637  fourierdlem102  46654  fourierdlem114  46666  iooborel  46797  hoicvrrex  47002  lamberte  47348