Theorem sselii 3884

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

Syntax hints:   ∈ wcel 2112   ⊆ wss 3853

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 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  sseliALT  5187  fvrn0  6723  ovima0  7365  brtpos0  7953  frrlem14  8018  wfrlem16  8048  rdg0  8135  iunfi  8942  rankdmr1  9382  rankeq0b  9441  cardprclem  9560  alephfp2  9688  dfac2b  9709  sdom2en01  9881  fin56  9972  fin1a2lem10  9988  hsmexlem4  10008  canthp1lem2  10232  ax1cn  10728  recni  10812  0xr  10845  pnfxr  10852  nn0rei  12066  nn0cni  12067  0xnn0  12133  nnzi  12166  nn0zi  12167  seqexw  13555  mulgfval  18444  lbsextlem4  20152  qsubdrg  20369  leordtval2  22063  iooordt  22068  hauspwdom  22352  comppfsc  22383  dfac14  22469  filconn  22734  isufil2  22759  iooretop  23617  ovolfiniun  24352  volfiniun  24398  iblabslem  24679  iblabs  24680  bddmulibl  24690  mdegcl  24921  logcn  25489  logccv  25505  leibpi  25779  xrlimcnp  25805  jensen  25825  emre  25842  lgsdir2lem3  26162  shelii  29250  chelii  29268  omlsilem  29437  nonbooli  29686  pjssmii  29716  riesz4  30099  riesz1  30100  cnlnadjeu  30113  nmopadjlei  30123  adjeq0  30126  dp2clq  30829  rpdp2cl  30830  dp2lt10  30832  dp2lt  30833  dp2ltc  30835  dplti  30853  qqh0  31600  qqh1  31601  qqhcn  31607  rrh0  31631  esumcst  31697  esumrnmpt2  31702  volmeas  31865  hgt750lem  32297  tgoldbachgtde  32306  kur14lem7  32841  kur14lem9  32843  iinllyconn  32883  bj-pinftyccb  35076  bj-minftyccb  35080  bj-rrdrg  35144  finixpnum  35448  poimirlem32  35495  ftc1cnnclem  35534  ftc2nc  35545  areacirclem2  35552  prdsbnd  35637  reheibor  35683  rmxyadd  40387  rmxy1  40388  rmxy0  40389  rmydioph  40480  rmxdioph  40482  expdiophlem2  40488  expdioph  40489  mpaaeu  40619  fourierdlem85  43350  fourierdlem102  43367  fourierdlem114  43379  iooborel  43508  hoicvrrex  43712