Theorem sselii 3927

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3898

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 2808  df-ss 3915

This theorem is referenced by:  sseliALT  5251  fvrn0  6859  ovima0  7534  brtpos0  8172  frrlem14  8238  rdg0  8349  iunfi  9238  rankdmr1  9705  rankeq0b  9764  cardprclem  9883  alephfp2  10011  dfac2b  10033  sdom2en01  10204  fin56  10295  fin1a2lem10  10311  hsmexlem4  10331  canthp1lem2  10555  ax1cn  11051  recni  11137  0xr  11170  pnfxr  11177  nn0rei  12403  nn0cni  12404  0xnn0  12471  nnzi  12506  nn0zi  12507  seqexw  13931  mulgfval  18990  lbsextlem4  21107  qsubdrg  21365  leordtval2  23147  iooordt  23152  hauspwdom  23436  comppfsc  23467  dfac14  23553  filconn  23818  isufil2  23843  iooretop  24700  ovolfiniun  25449  volfiniun  25495  iblabslem  25776  iblabs  25777  bddmulibl  25787  mdegcl  26021  logcn  26603  logccv  26619  leibpi  26899  xrlimcnp  26925  jensen  26946  emre  26963  lgsdir2lem3  27285  shelii  31216  chelii  31234  omlsilem  31403  nonbooli  31652  pjssmii  31682  riesz4  32065  riesz1  32066  cnlnadjeu  32079  nmopadjlei  32089  adjeq0  32092  dp2clq  32890  rpdp2cl  32891  dp2lt10  32893  dp2lt  32894  dp2ltc  32896  dplti  32914  zringfrac  33563  vieta  33664  qqh0  34069  qqh1  34070  qqhcn  34076  rrh0  34100  esumcst  34148  esumrnmpt2  34153  volmeas  34316  hgt750lem  34736  tgoldbachgtde  34745  kur14lem7  35328  kur14lem9  35330  iinllyconn  35370  bj-rdg0gALT  37188  bj-pinftyccb  37338  bj-minftyccb  37342  bj-rrdrg  37407  finixpnum  37718  poimirlem32  37765  ftc1cnnclem  37804  ftc2nc  37815  areacirclem2  37822  prdsbnd  37906  reheibor  37952  rmxyadd  43078  rmxy1  43079  rmxy0  43080  rmydioph  43171  rmxdioph  43173  expdiophlem2  43179  expdioph  43180  mpaaeu  43307  0iscard  43698  1iscard  43699  wfaxrep  45151  wfaxnul  45153  wfaxinf2  45158  fourierdlem85  46351  fourierdlem102  46368  fourierdlem114  46380  iooborel  46511  hoicvrrex  46716  lamberte  47050