Theorem sselii 3918

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

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

This theorem is referenced by:  sseliALT  5244  fvrn0  6868  ovima0  7546  brtpos0  8183  frrlem14  8249  rdg0  8360  iunfi  9253  rankdmr1  9725  rankeq0b  9784  cardprclem  9903  alephfp2  10031  dfac2b  10053  sdom2en01  10224  fin56  10315  fin1a2lem10  10331  hsmexlem4  10351  canthp1lem2  10576  ax1cn  11072  recni  11159  0xr  11192  pnfxr  11199  nn0rei  12448  nn0cni  12449  0xnn0  12516  nnzi  12551  nn0zi  12552  seqexw  13979  mulgfval  19045  lbsextlem4  21159  qsubdrg  21399  leordtval2  23177  iooordt  23182  hauspwdom  23466  comppfsc  23497  dfac14  23583  filconn  23848  isufil2  23873  iooretop  24730  ovolfiniun  25468  volfiniun  25514  iblabslem  25795  iblabs  25796  bddmulibl  25806  mdegcl  26034  logcn  26611  logccv  26627  leibpi  26906  xrlimcnp  26932  jensen  26952  emre  26969  lgsdir2lem3  27290  shelii  31286  chelii  31304  omlsilem  31473  nonbooli  31722  pjssmii  31752  riesz4  32135  riesz1  32136  cnlnadjeu  32149  nmopadjlei  32159  adjeq0  32162  dp2clq  32940  rpdp2cl  32941  dp2lt10  32943  dp2lt  32944  dp2ltc  32946  dplti  32964  zringfrac  33614  vieta  33724  qqh0  34128  qqh1  34129  qqhcn  34135  rrh0  34159  esumcst  34207  esumrnmpt2  34212  volmeas  34375  hgt750lem  34795  tgoldbachgtde  34804  kur14lem7  35394  kur14lem9  35396  iinllyconn  35436  bj-rdg0gALT  37378  bj-pinftyccb  37535  bj-minftyccb  37539  bj-rrdrg  37604  finixpnum  37926  poimirlem32  37973  ftc1cnnclem  38012  ftc2nc  38023  areacirclem2  38030  prdsbnd  38114  reheibor  38160  rmxyadd  43349  rmxy1  43350  rmxy0  43351  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  mpaaeu  43578  0iscard  43968  1iscard  43969  wfaxrep  45421  wfaxnul  45423  wfaxinf2  45428  fourierdlem85  46619  fourierdlem102  46636  fourierdlem114  46648  iooborel  46779  hoicvrrex  46984  lamberte  47336