Theorem sselii 3926

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

Syntax hints:   ∈ wcel 2111   ⊆ wss 3897

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 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3914

This theorem is referenced by:  sseliALT  5242  fvrn0  6845  ovima0  7520  brtpos0  8158  frrlem14  8224  rdg0  8335  iunfi  9222  rankdmr1  9689  rankeq0b  9748  cardprclem  9867  alephfp2  9995  dfac2b  10017  sdom2en01  10188  fin56  10279  fin1a2lem10  10295  hsmexlem4  10315  canthp1lem2  10539  ax1cn  11035  recni  11121  0xr  11154  pnfxr  11161  nn0rei  12387  nn0cni  12388  0xnn0  12455  nnzi  12491  nn0zi  12492  seqexw  13919  mulgfval  18977  lbsextlem4  21093  qsubdrg  21351  leordtval2  23122  iooordt  23127  hauspwdom  23411  comppfsc  23442  dfac14  23528  filconn  23793  isufil2  23818  iooretop  24675  ovolfiniun  25424  volfiniun  25470  iblabslem  25751  iblabs  25752  bddmulibl  25762  mdegcl  25996  logcn  26578  logccv  26594  leibpi  26874  xrlimcnp  26900  jensen  26921  emre  26938  lgsdir2lem3  27260  shelii  31187  chelii  31205  omlsilem  31374  nonbooli  31623  pjssmii  31653  riesz4  32036  riesz1  32037  cnlnadjeu  32050  nmopadjlei  32060  adjeq0  32063  dp2clq  32853  rpdp2cl  32854  dp2lt10  32856  dp2lt  32857  dp2ltc  32859  dplti  32877  zringfrac  33511  qqh0  33989  qqh1  33990  qqhcn  33996  rrh0  34020  esumcst  34068  esumrnmpt2  34073  volmeas  34236  hgt750lem  34656  tgoldbachgtde  34665  kur14lem7  35248  kur14lem9  35250  iinllyconn  35290  bj-rdg0gALT  37105  bj-pinftyccb  37255  bj-minftyccb  37259  bj-rrdrg  37324  finixpnum  37645  poimirlem32  37692  ftc1cnnclem  37731  ftc2nc  37742  areacirclem2  37749  prdsbnd  37833  reheibor  37879  rmxyadd  42954  rmxy1  42955  rmxy0  42956  rmydioph  43047  rmxdioph  43049  expdiophlem2  43055  expdioph  43056  mpaaeu  43183  0iscard  43574  1iscard  43575  wfaxrep  45027  wfaxnul  45029  wfaxinf2  45034  fourierdlem85  46229  fourierdlem102  46246  fourierdlem114  46258  iooborel  46389  hoicvrrex  46594  lamberte  46919