Theorem sselii 3913

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

Syntax hints:   ∈ wcel 2121   ⊆ wss 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-clel 2816  df-ss 3901

This theorem is referenced by:  sseliALT  5233  fvrn0  6858  ovima0  7538  brtpos0  8175  frrlem14  8242  rdg0  8354  iunfi  9247  rankdmr1  9720  rankeq0b  9779  cardprclem  9898  alephfp2  10026  dfac2b  10048  sdom2en01  10220  fin56  10311  fin1a2lem10  10327  hsmexlem4  10347  canthp1lem2  10572  ax1cn  11068  recni  11155  0xr  11188  pnfxr  11195  nn0rei  12443  nn0cni  12444  0xnn0  12511  nnzi  12546  nn0zi  12547  seqexw  13974  mulgfval  19040  lbsextlem4  21157  qsubdrg  21397  leordtval2  23198  iooordt  23203  hauspwdom  23487  comppfsc  23518  dfac14  23604  filconn  23869  isufil2  23894  iooretop  24751  ovolfiniun  25489  volfiniun  25535  iblabslem  25816  iblabs  25817  bddmulibl  25827  mdegcl  26055  logcn  26632  logccv  26648  leibpi  26927  xrlimcnp  26953  jensen  26973  emre  26990  lgsdir2lem3  27311  shelii  31306  chelii  31324  omlsilem  31493  nonbooli  31742  pjssmii  31772  riesz4  32155  riesz1  32156  cnlnadjeu  32169  nmopadjlei  32179  adjeq0  32182  dp2clq  32961  rpdp2cl  32962  dp2lt10  32964  dp2lt  32965  dp2ltc  32967  dplti  32985  zringfrac  33647  vieta  33774  qqh0  34178  qqh1  34179  qqhcn  34185  rrh0  34209  esumcst  34257  esumrnmpt2  34262  volmeas  34425  hgt750lem  34845  tgoldbachgtde  34854  kur14lem7  35453  kur14lem9  35455  iinllyconn  35495  bj-rdg0gALT  37437  bj-pinftyccb  37594  bj-minftyccb  37598  bj-rrdrg  37663  finixpnum  37985  poimirlem32  38032  ftc1cnnclem  38071  ftc2nc  38082  areacirclem2  38089  prdsbnd  38173  reheibor  38219  rmxyadd  43379  rmxy1  43380  rmxy0  43381  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  expdioph  43481  mpaaeu  43608  0iscard  43998  1iscard  43999  wfaxrep  45451  wfaxnul  45453  wfaxinf2  45458  fourierdlem85  46646  fourierdlem102  46663  fourierdlem114  46675  iooborel  46806  hoicvrrex  47011  lamberte  47363