Theorem sselii 3943

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3914

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 3931

This theorem is referenced by:  sseliALT  5264  fvrn0  6888  ovima0  7568  brtpos0  8212  frrlem14  8278  rdg0  8389  iunfi  9294  rankdmr1  9754  rankeq0b  9813  cardprclem  9932  alephfp2  10062  dfac2b  10084  sdom2en01  10255  fin56  10346  fin1a2lem10  10362  hsmexlem4  10382  canthp1lem2  10606  ax1cn  11102  recni  11188  0xr  11221  pnfxr  11228  nn0rei  12453  nn0cni  12454  0xnn0  12521  nnzi  12557  nn0zi  12558  seqexw  13982  mulgfval  19001  lbsextlem4  21071  qsubdrg  21336  leordtval2  23099  iooordt  23104  hauspwdom  23388  comppfsc  23419  dfac14  23505  filconn  23770  isufil2  23795  iooretop  24653  ovolfiniun  25402  volfiniun  25448  iblabslem  25729  iblabs  25730  bddmulibl  25740  mdegcl  25974  logcn  26556  logccv  26572  leibpi  26852  xrlimcnp  26878  jensen  26899  emre  26916  lgsdir2lem3  27238  shelii  31144  chelii  31162  omlsilem  31331  nonbooli  31580  pjssmii  31610  riesz4  31993  riesz1  31994  cnlnadjeu  32007  nmopadjlei  32017  adjeq0  32020  dp2clq  32801  rpdp2cl  32802  dp2lt10  32804  dp2lt  32805  dp2ltc  32807  dplti  32825  zringfrac  33525  qqh0  33974  qqh1  33975  qqhcn  33981  rrh0  34005  esumcst  34053  esumrnmpt2  34058  volmeas  34221  hgt750lem  34642  tgoldbachgtde  34651  kur14lem7  35199  kur14lem9  35201  iinllyconn  35241  bj-rdg0gALT  37059  bj-pinftyccb  37209  bj-minftyccb  37213  bj-rrdrg  37278  finixpnum  37599  poimirlem32  37646  ftc1cnnclem  37685  ftc2nc  37696  areacirclem2  37703  prdsbnd  37787  reheibor  37833  rmxyadd  42910  rmxy1  42911  rmxy0  42912  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  mpaaeu  43139  0iscard  43530  1iscard  43531  wfaxrep  44984  wfaxnul  44986  wfaxinf2  44991  fourierdlem85  46189  fourierdlem102  46206  fourierdlem114  46218  iooborel  46349  hoicvrrex  46554  lamberte  46889