Theorem sselii 3979

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

Syntax hints:   ∈ wcel 2106   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  sseliALT  5309  fvrn0  6921  ovima0  7588  brtpos0  8220  frrlem14  8286  wfrlem16OLD  8326  rdg0  8423  iunfi  9342  rankdmr1  9798  rankeq0b  9857  cardprclem  9976  alephfp2  10106  dfac2b  10127  sdom2en01  10299  fin56  10390  fin1a2lem10  10406  hsmexlem4  10426  canthp1lem2  10650  ax1cn  11146  recni  11232  0xr  11265  pnfxr  11272  nn0rei  12487  nn0cni  12488  0xnn0  12554  nnzi  12590  nn0zi  12591  seqexw  13986  mulgfval  18988  lbsextlem4  20919  qsubdrg  21197  leordtval2  22936  iooordt  22941  hauspwdom  23225  comppfsc  23256  dfac14  23342  filconn  23607  isufil2  23632  iooretop  24502  ovolfiniun  25242  volfiniun  25288  iblabslem  25569  iblabs  25570  bddmulibl  25580  mdegcl  25811  logcn  26379  logccv  26395  leibpi  26671  xrlimcnp  26697  jensen  26717  emre  26734  lgsdir2lem3  27054  shelii  30723  chelii  30741  omlsilem  30910  nonbooli  31159  pjssmii  31189  riesz4  31572  riesz1  31573  cnlnadjeu  31586  nmopadjlei  31596  adjeq0  31599  dp2clq  32302  rpdp2cl  32303  dp2lt10  32305  dp2lt  32306  dp2ltc  32308  dplti  32326  qqh0  33250  qqh1  33251  qqhcn  33257  rrh0  33281  esumcst  33347  esumrnmpt2  33352  volmeas  33515  hgt750lem  33949  tgoldbachgtde  33958  kur14lem7  34489  kur14lem9  34491  iinllyconn  34531  bj-rdg0gALT  36255  bj-pinftyccb  36405  bj-minftyccb  36409  bj-rrdrg  36474  finixpnum  36776  poimirlem32  36823  ftc1cnnclem  36862  ftc2nc  36873  areacirclem2  36880  prdsbnd  36964  reheibor  37010  rmxyadd  41962  rmxy1  41963  rmxy0  41964  rmydioph  42055  rmxdioph  42057  expdiophlem2  42063  expdioph  42064  mpaaeu  42194  0iscard  42594  1iscard  42595  fourierdlem85  45206  fourierdlem102  45223  fourierdlem114  45235  iooborel  45366  hoicvrrex  45571