Theorem sselii 3973

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

Syntax hints:   ∈ wcel 2098   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2802  df-ss 3961

This theorem is referenced by:  sseliALT  5310  fvrn0  6926  ovima0  7600  brtpos0  8239  frrlem14  8305  wfrlem16OLD  8345  rdg0  8442  iunfi  9366  rankdmr1  9826  rankeq0b  9885  cardprclem  10004  alephfp2  10134  dfac2b  10155  sdom2en01  10327  fin56  10418  fin1a2lem10  10434  hsmexlem4  10454  canthp1lem2  10678  ax1cn  11174  recni  11260  0xr  11293  pnfxr  11300  nn0rei  12516  nn0cni  12517  0xnn0  12583  nnzi  12619  nn0zi  12620  seqexw  14018  mulgfval  19033  lbsextlem4  21061  qsubdrg  21369  leordtval2  23160  iooordt  23165  hauspwdom  23449  comppfsc  23480  dfac14  23566  filconn  23831  isufil2  23856  iooretop  24726  ovolfiniun  25474  volfiniun  25520  iblabslem  25801  iblabs  25802  bddmulibl  25812  mdegcl  26049  logcn  26626  logccv  26642  leibpi  26919  xrlimcnp  26945  jensen  26966  emre  26983  lgsdir2lem3  27305  shelii  31097  chelii  31115  omlsilem  31284  nonbooli  31533  pjssmii  31563  riesz4  31946  riesz1  31947  cnlnadjeu  31960  nmopadjlei  31970  adjeq0  31973  dp2clq  32689  rpdp2cl  32690  dp2lt10  32692  dp2lt  32693  dp2ltc  32695  dplti  32713  zringfrac  33369  qqh0  33716  qqh1  33717  qqhcn  33723  rrh0  33747  esumcst  33813  esumrnmpt2  33818  volmeas  33981  hgt750lem  34414  tgoldbachgtde  34423  kur14lem7  34953  kur14lem9  34955  iinllyconn  34995  bj-rdg0gALT  36681  bj-pinftyccb  36831  bj-minftyccb  36835  bj-rrdrg  36900  finixpnum  37209  poimirlem32  37256  ftc1cnnclem  37295  ftc2nc  37306  areacirclem2  37313  prdsbnd  37397  reheibor  37443  rmxyadd  42484  rmxy1  42485  rmxy0  42486  rmydioph  42577  rmxdioph  42579  expdiophlem2  42585  expdioph  42586  mpaaeu  42716  0iscard  43113  1iscard  43114  fourierdlem85  45717  fourierdlem102  45734  fourierdlem114  45746  iooborel  45877  hoicvrrex  46082