Theorem sselii 3946

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3917

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 2804  df-ss 3934

This theorem is referenced by:  sseliALT  5267  fvrn0  6891  ovima0  7571  brtpos0  8215  frrlem14  8281  rdg0  8392  iunfi  9301  rankdmr1  9761  rankeq0b  9820  cardprclem  9939  alephfp2  10069  dfac2b  10091  sdom2en01  10262  fin56  10353  fin1a2lem10  10369  hsmexlem4  10389  canthp1lem2  10613  ax1cn  11109  recni  11195  0xr  11228  pnfxr  11235  nn0rei  12460  nn0cni  12461  0xnn0  12528  nnzi  12564  nn0zi  12565  seqexw  13989  mulgfval  19008  lbsextlem4  21078  qsubdrg  21343  leordtval2  23106  iooordt  23111  hauspwdom  23395  comppfsc  23426  dfac14  23512  filconn  23777  isufil2  23802  iooretop  24660  ovolfiniun  25409  volfiniun  25455  iblabslem  25736  iblabs  25737  bddmulibl  25747  mdegcl  25981  logcn  26563  logccv  26579  leibpi  26859  xrlimcnp  26885  jensen  26906  emre  26923  lgsdir2lem3  27245  shelii  31151  chelii  31169  omlsilem  31338  nonbooli  31587  pjssmii  31617  riesz4  32000  riesz1  32001  cnlnadjeu  32014  nmopadjlei  32024  adjeq0  32027  dp2clq  32808  rpdp2cl  32809  dp2lt10  32811  dp2lt  32812  dp2ltc  32814  dplti  32832  zringfrac  33532  qqh0  33981  qqh1  33982  qqhcn  33988  rrh0  34012  esumcst  34060  esumrnmpt2  34065  volmeas  34228  hgt750lem  34649  tgoldbachgtde  34658  kur14lem7  35206  kur14lem9  35208  iinllyconn  35248  bj-rdg0gALT  37066  bj-pinftyccb  37216  bj-minftyccb  37220  bj-rrdrg  37285  finixpnum  37606  poimirlem32  37653  ftc1cnnclem  37692  ftc2nc  37703  areacirclem2  37710  prdsbnd  37794  reheibor  37840  rmxyadd  42917  rmxy1  42918  rmxy0  42919  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  mpaaeu  43146  0iscard  43537  1iscard  43538  wfaxrep  44991  wfaxnul  44993  wfaxinf2  44998  fourierdlem85  46196  fourierdlem102  46213  fourierdlem114  46225  iooborel  46356  hoicvrrex  46561  lamberte  46896