Theorem sselii 3940

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3928

This theorem is referenced by:  sseliALT  5259  fvrn0  6870  ovima0  7548  brtpos0  8189  frrlem14  8255  rdg0  8366  iunfi  9270  rankdmr1  9730  rankeq0b  9789  cardprclem  9908  alephfp2  10038  dfac2b  10060  sdom2en01  10231  fin56  10322  fin1a2lem10  10338  hsmexlem4  10358  canthp1lem2  10582  ax1cn  11078  recni  11164  0xr  11197  pnfxr  11204  nn0rei  12429  nn0cni  12430  0xnn0  12497  nnzi  12533  nn0zi  12534  seqexw  13958  mulgfval  18977  lbsextlem4  21047  qsubdrg  21312  leordtval2  23075  iooordt  23080  hauspwdom  23364  comppfsc  23395  dfac14  23481  filconn  23746  isufil2  23771  iooretop  24629  ovolfiniun  25378  volfiniun  25424  iblabslem  25705  iblabs  25706  bddmulibl  25716  mdegcl  25950  logcn  26532  logccv  26548  leibpi  26828  xrlimcnp  26854  jensen  26875  emre  26892  lgsdir2lem3  27214  shelii  31117  chelii  31135  omlsilem  31304  nonbooli  31553  pjssmii  31583  riesz4  31966  riesz1  31967  cnlnadjeu  31980  nmopadjlei  31990  adjeq0  31993  dp2clq  32774  rpdp2cl  32775  dp2lt10  32777  dp2lt  32778  dp2ltc  32780  dplti  32798  zringfrac  33498  qqh0  33947  qqh1  33948  qqhcn  33954  rrh0  33978  esumcst  34026  esumrnmpt2  34031  volmeas  34194  hgt750lem  34615  tgoldbachgtde  34624  kur14lem7  35172  kur14lem9  35174  iinllyconn  35214  bj-rdg0gALT  37032  bj-pinftyccb  37182  bj-minftyccb  37186  bj-rrdrg  37251  finixpnum  37572  poimirlem32  37619  ftc1cnnclem  37658  ftc2nc  37669  areacirclem2  37676  prdsbnd  37760  reheibor  37806  rmxyadd  42883  rmxy1  42884  rmxy0  42885  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  expdioph  42985  mpaaeu  43112  0iscard  43503  1iscard  43504  wfaxrep  44957  wfaxnul  44959  wfaxinf2  44964  fourierdlem85  46162  fourierdlem102  46179  fourierdlem114  46191  iooborel  46322  hoicvrrex  46527  lamberte  46862