Theorem sselii 3930

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3901

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 2115

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

This theorem is referenced by:  sseliALT  5254  fvrn0  6862  ovima0  7537  brtpos0  8175  frrlem14  8241  rdg0  8352  iunfi  9243  rankdmr1  9713  rankeq0b  9772  cardprclem  9891  alephfp2  10019  dfac2b  10041  sdom2en01  10212  fin56  10303  fin1a2lem10  10319  hsmexlem4  10339  canthp1lem2  10564  ax1cn  11060  recni  11146  0xr  11179  pnfxr  11186  nn0rei  12412  nn0cni  12413  0xnn0  12480  nnzi  12515  nn0zi  12516  seqexw  13940  mulgfval  18999  lbsextlem4  21116  qsubdrg  21374  leordtval2  23156  iooordt  23161  hauspwdom  23445  comppfsc  23476  dfac14  23562  filconn  23827  isufil2  23852  iooretop  24709  ovolfiniun  25458  volfiniun  25504  iblabslem  25785  iblabs  25786  bddmulibl  25796  mdegcl  26030  logcn  26612  logccv  26628  leibpi  26908  xrlimcnp  26934  jensen  26955  emre  26972  lgsdir2lem3  27294  shelii  31290  chelii  31308  omlsilem  31477  nonbooli  31726  pjssmii  31756  riesz4  32139  riesz1  32140  cnlnadjeu  32153  nmopadjlei  32163  adjeq0  32166  dp2clq  32962  rpdp2cl  32963  dp2lt10  32965  dp2lt  32966  dp2ltc  32968  dplti  32986  zringfrac  33635  vieta  33736  qqh0  34141  qqh1  34142  qqhcn  34148  rrh0  34172  esumcst  34220  esumrnmpt2  34225  volmeas  34388  hgt750lem  34808  tgoldbachgtde  34817  kur14lem7  35406  kur14lem9  35408  iinllyconn  35448  exeltr  36665  bj-rdg0gALT  37272  bj-pinftyccb  37426  bj-minftyccb  37430  bj-rrdrg  37495  finixpnum  37806  poimirlem32  37853  ftc1cnnclem  37892  ftc2nc  37903  areacirclem2  37910  prdsbnd  37994  reheibor  38040  rmxyadd  43163  rmxy1  43164  rmxy0  43165  rmydioph  43256  rmxdioph  43258  expdiophlem2  43264  expdioph  43265  mpaaeu  43392  0iscard  43782  1iscard  43783  wfaxrep  45235  wfaxnul  45237  wfaxinf2  45242  fourierdlem85  46435  fourierdlem102  46452  fourierdlem114  46464  iooborel  46595  hoicvrrex  46800  lamberte  47134