Theorem sseld 2119

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 2115	. 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 994   (_ wss 2099

This theorem is referenced by:  sseldd 2120  ssbrd 2729  uniopel 2886  elrel 3342  dmrnssfld 3444  nfunv 3651  opelf 3747  fvimacnv 3919  ffvelrn 3928  1stdm 4169  oa00 4329  omordi 4333  omlimcl 4345  mapsn 4486  ixpf 4497  uniixp 4498  pssnn 4681  sucprcreg 4743  inf3lem2 4759  trcl 4791  r1ord 4801  rankwflem 4811  rankr1 4820  ssrankr1 4822  rankel 4826  r1pwcl 4833  rankuni2 4836  rankval4 4848  cplem1 4866  kmlem2 4912  zorn2lem7 4940  carduniima 5040  alephfp 5050  elprpq 5249  genpss 5261  ltexprlem7 5302  suprub 6224  uzind 6376  elfzp1 6641  fsequb 6654  fsequb2 6655  seqzfveq 6749  fsump1s 7216  fsumcllem 7217  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsummulc1 7236  fsumcmp 7243  fsumcmpndx2 7245  fsumabs 7246  fsum0diaglem2 7462  fsum0diag2 7464  fsum0diag3 7465  fsum0diag4 7466  infxpidmlem5 7768  infxpidmlem7 7770  infxpidmlem8 7771  unitg 7835  tgss2 7849  elcls 7914  clsndisj 7916  elcls3 7921  neindisj 7941  lpval 7953  lpsscls 7955  clslp 7958  cncnpi 7983  cncnp 7988  opni2 8075  rnblopn 8084  caussi 8165  bcthlem28 8237  subgabl 8365  nmcn3 8595  nmcnc 8596  sspmval 8646  sspival 8651  sspimsval 8653  sspph 8771  ubthlem6 8792  shel 9356  shsubcl 9365  shsubclOLD 9366  chel 9376  ocorth 9440  shorth 9444  shsel 9554  elspansn3 9771  elnlfn2 10133  sumdmdlem2 10628  bepart 10800  dmrngcmp 11205  elfiun 11421  fictblem 11422  ordtypelem6 11432  subntr 11482  cptclsscpt 11489  compfipin0lem 11492  alexsublem4 11499  alexsub 11500  subtopmetlem 11505  subtopmet 11506  reconnlem4 11510  reconnlem5 11511  iccconn 11514  neibastop2lem2 11581  fnejoin1 11591  fnejoin2 11592  fbfgss 11640  uffixfr 11660  flimnei 11678  elfilmap2 11691  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  flimfbas 11713  isfclus 11718  fclusbas 11722  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscomp 11733  tailuni 11761  fzm1 11867  lpss2 11906  mettrifi2 11913  geomcau 11914  iccsplit 11919  lincmb01icc 11943  lmtlm 11969  tx1cn 11976  tx2cn 11977  sstotbnd 11992  totbndbnd 12000  ismtyhmeolem 12006  heiborlem1 12011  heiborlem15 12025  heiborlem16 12026  recms 12066  iccbnd 12082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain