Theorem sselii 3934

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3905

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 3922

This theorem is referenced by:  sseliALT  5251  fvrn0  6854  ovima0  7532  brtpos0  8173  frrlem14  8239  rdg0  8350  iunfi  9252  rankdmr1  9716  rankeq0b  9775  cardprclem  9894  alephfp2  10022  dfac2b  10044  sdom2en01  10215  fin56  10306  fin1a2lem10  10322  hsmexlem4  10342  canthp1lem2  10566  ax1cn  11062  recni  11148  0xr  11181  pnfxr  11188  nn0rei  12414  nn0cni  12415  0xnn0  12482  nnzi  12518  nn0zi  12519  seqexw  13943  mulgfval  18967  lbsextlem4  21087  qsubdrg  21345  leordtval2  23116  iooordt  23121  hauspwdom  23405  comppfsc  23436  dfac14  23522  filconn  23787  isufil2  23812  iooretop  24670  ovolfiniun  25419  volfiniun  25465  iblabslem  25746  iblabs  25747  bddmulibl  25757  mdegcl  25991  logcn  26573  logccv  26589  leibpi  26869  xrlimcnp  26895  jensen  26916  emre  26933  lgsdir2lem3  27255  shelii  31178  chelii  31196  omlsilem  31365  nonbooli  31614  pjssmii  31644  riesz4  32027  riesz1  32028  cnlnadjeu  32041  nmopadjlei  32051  adjeq0  32054  dp2clq  32840  rpdp2cl  32841  dp2lt10  32843  dp2lt  32844  dp2ltc  32846  dplti  32864  zringfrac  33510  qqh0  33970  qqh1  33971  qqhcn  33977  rrh0  34001  esumcst  34049  esumrnmpt2  34054  volmeas  34217  hgt750lem  34638  tgoldbachgtde  34647  kur14lem7  35204  kur14lem9  35206  iinllyconn  35246  bj-rdg0gALT  37064  bj-pinftyccb  37214  bj-minftyccb  37218  bj-rrdrg  37283  finixpnum  37604  poimirlem32  37651  ftc1cnnclem  37690  ftc2nc  37701  areacirclem2  37708  prdsbnd  37792  reheibor  37838  rmxyadd  42914  rmxy1  42915  rmxy0  42916  rmydioph  43007  rmxdioph  43009  expdiophlem2  43015  expdioph  43016  mpaaeu  43143  0iscard  43534  1iscard  43535  wfaxrep  44988  wfaxnul  44990  wfaxinf2  44995  fourierdlem85  46192  fourierdlem102  46209  fourierdlem114  46221  iooborel  46352  hoicvrrex  46557  lamberte  46892