Theorem sseld 2038

Description: Membership deduction from subclass relationship.

Hypothesis

Ref	Expression
sseld.1	|- (ph -> A (_ B)

Assertion

Ref	Expression
sseld	|- (ph -> (C e. A -> C e. B))

Proof of Theorem sseld

Step	Hyp	Ref	Expression
1		sseld.1	. 2 |- (ph -> A (_ B)
2		ssel 2034	. 2 |- (A (_ B -> (C e. A -> C e. B))
3	1, 2	syl 10	1 |- (ph -> (C e. A -> C e. B))

Syntax hints:   -> wi 3   e. wcel 1105   (_ wss 2018

This theorem is referenced by:  sseldd 2039  ssbrd 2624  elrel 3215  unielrel 3456  relfld 3457  nfunv 3487  opelf 3579  fvimacnv 3744  ffvelrn 3753  1stdm 4047  oa00 4131  omordi 4135  omlimcl 4147  mapsn 4283  ixpf 4294  uniixp 4295  pssnn 4465  sucprcreg 4524  inf3lem2 4538  trcl 4569  r1ord 4579  rankwflem 4589  rankr1 4598  ssrankr1 4600  rankel 4604  r1pwcl 4611  rankuni2 4614  rankval4 4626  cplem1 4644  kmlem2 4690  zorn2lem7 4718  carduniima 4813  alephfp 4823  elprpq 5018  genpss 5030  ltexprlem7 5071  suprub 5954  uzind 6104  elfzp1 6393  fsequb 6406  fsequb2 6407  seqzfveq 6437  fsump1s 6902  fsumcllem 6903  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  fsumcom 6917  fsumrev 6918  fsummulc1 6922  fsumcmp 6929  fsumcmpndx2 6931  fsumabs 6932  fsum0diaglem2 7143  fsum0diag2 7145  fsum0diag3 7146  fsum0diag4 7147  infxpidmlem5 7450  infxpidmlem7 7452  infxpidmlem8 7453  unitgt 7516  tgss2t 7530  elcls 7596  clsndisj 7598  elcls3 7600  neindisj 7620  lpval 7632  lpsscls 7634  clslp 7637  cncnpi 7660  cncnp 7665  opni2 7753  rnblopn 7762  caussi 7837  bcthlem28 7908  subgabl 8008  nmcnc 8213  sspmval 8261  sspival 8266  sspimsval 8268  sspph 8381  ubthlem6 8400  shelt 9231  shsubclt 9240  shsubcltOLD 9241  chelt 9251  ocorth 9294  shorth 9298  shselt 9407  elspansn3t 9626  elnlfn2t 9983  sumdmdlem2 10467

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-in 2022  df-ss 2024

Copyright terms: Public domain