Theorem sselii 3927

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

Syntax hints:   ∈ wcel 2105   ⊆ wss 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3903  df-ss 3913

This theorem is referenced by:  sseliALT  5246  fvrn0  6839  ovima0  7489  brtpos0  8094  frrlem14  8160  wfrlem16OLD  8200  rdg0  8297  iunfi  9175  rankdmr1  9627  rankeq0b  9686  cardprclem  9805  alephfp2  9935  dfac2b  9956  sdom2en01  10128  fin56  10219  fin1a2lem10  10235  hsmexlem4  10255  canthp1lem2  10479  ax1cn  10975  recni  11059  0xr  11092  pnfxr  11099  nn0rei  12314  nn0cni  12315  0xnn0  12381  nnzi  12414  nn0zi  12415  seqexw  13807  mulgfval  18769  lbsextlem4  20494  qsubdrg  20721  leordtval2  22434  iooordt  22439  hauspwdom  22723  comppfsc  22754  dfac14  22840  filconn  23105  isufil2  23130  iooretop  24000  ovolfiniun  24736  volfiniun  24782  iblabslem  25063  iblabs  25064  bddmulibl  25074  mdegcl  25305  logcn  25873  logccv  25889  leibpi  26163  xrlimcnp  26189  jensen  26209  emre  26226  lgsdir2lem3  26546  shelii  29685  chelii  29703  omlsilem  29872  nonbooli  30121  pjssmii  30151  riesz4  30534  riesz1  30535  cnlnadjeu  30548  nmopadjlei  30558  adjeq0  30561  dp2clq  31263  rpdp2cl  31264  dp2lt10  31266  dp2lt  31267  dp2ltc  31269  dplti  31287  qqh0  32040  qqh1  32041  qqhcn  32047  rrh0  32071  esumcst  32137  esumrnmpt2  32142  volmeas  32305  hgt750lem  32737  tgoldbachgtde  32746  kur14lem7  33280  kur14lem9  33282  iinllyconn  33322  bj-rdg0gALT  35302  bj-pinftyccb  35452  bj-minftyccb  35456  bj-rrdrg  35521  finixpnum  35822  poimirlem32  35869  ftc1cnnclem  35908  ftc2nc  35919  areacirclem2  35926  prdsbnd  36011  reheibor  36057  rmxyadd  40954  rmxy1  40955  rmxy0  40956  rmydioph  41047  rmxdioph  41049  expdiophlem2  41055  expdioph  41056  mpaaeu  41186  0iscard  41376  1iscard  41377  fourierdlem85  43976  fourierdlem102  43993  fourierdlem114  44005  iooborel  44134  hoicvrrex  44339