Theorem sseld 2067

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 2063	. 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 958   (_ wss 2047

This theorem is referenced by:  sseldd 2068  ssbrd 2656  uniopel 2809  elrel 3253  dmrnssfld 3357  nfunv 3546  opelf 3640  fvimacnv 3805  ffvelrn 3814  1stdm 4109  oa00 4193  omordi 4197  omlimcl 4209  mapsn 4345  ixpf 4356  uniixp 4357  pssnn 4534  sucprcreg 4600  inf3lem2 4614  trcl 4645  r1ord 4655  rankwflem 4665  rankr1 4674  ssrankr1 4676  rankel 4680  r1pwcl 4687  rankuni2 4690  rankval4 4702  cplem1 4720  kmlem2 4766  zorn2lem7 4794  carduniima 4890  alephfp 4900  elprpq 5095  genpss 5107  ltexprlem7 5148  suprub 6056  uzind 6205  elfzp1 6510  fsequb 6523  fsequb2 6524  seqzfveq 6554  fsump1s 7013  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag3 7260  fsum0diag4 7261  infxpidmlem5 7556  infxpidmlem7 7558  infxpidmlem8 7559  unitgt 7623  tgss2t 7637  elcls 7704  clsndisj 7706  elcls3 7711  neindisj 7731  lpval 7743  lpsscls 7745  clslp 7748  cncnpi 7773  cncnp 7778  opni2 7865  rnblopn 7874  caussi 7954  bcthlem28 8026  subgabl 8123  nmcn3 8341  nmcnc 8342  sspmval 8392  sspival 8397  sspimsval 8399  sspph 8515  ubthlem6 8534  shelt 9080  shsubclt 9089  shsubcltOLD 9090  chelt 9100  ocorth 9164  shorth 9168  shselt 9278  elspansn3t 9495  elnlfn2t 9853  sumdmdlem2 10346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain