Theorem sseld 1506

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 1502	. 2 |- (A (_ B -> (C e. A -> C e. B))
3	1, 2	syl 12	1 |- (ph -> (C e. A -> C e. B))

Syntax hints:   -> wi 2   e. wcel 1092   (_ wss 1487

This theorem is referenced by:  sseldd 1507  ssbrd 2094  nfunv 2693  opelf 2762  ffvrn 2890  oa00 3161  omordi 3164  mapsn 3269  pssnn 3428  sucprcreg 3451  inf3lem2 3465  trcl 3489  r1ord 3499  rankwflem 3509  rankr1 3518  ssrankr1 3520  rankel 3524  r1pwcl 3530  rankuni 3533  ranklon 3540  cplem1 3545  kmlem2 3581  zornlem7 3609  carduniima 3695  elprpq 3889  genpss 3901  ltexprlem7 3942  suprub 4513  infxpidmlem5 4937  infxpidmlem7 4939  infxpidmlem8 4940  shelt 5118  shsubclt 5125  chelt 5135  ocorth 5172  shorth 5176  shselt 5280  elspansn3t 5477  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org