Theorem ssel 1502

Description: Membership relationships follow from a subclass relationship.

Assertion

Ref	Expression
ssel	|- (A (_ B -> (C e. A -> C e. B))

Proof of Theorem ssel

Step	Hyp	Ref	Expression
1		dfss2 1497	. . . . . 6 |- (A (_ B <-> A.x(x e. A -> x e. B))
2	1	biimp 133	. . . . 5 |- (A (_ B -> A.x(x e. A -> x e. B))
3	2	19.21bi 742	. . . 4 |- (A (_ B -> (x e. A -> x e. B))
4	3	anim2d 433	. . 3 |- (A (_ B -> ((x = C /\ x e. A) -> (x = C /\ x e. B)))
5	4	19.22dv 947	. 2 |- (A (_ B -> (E.x(x = C /\ x e. A) -> E.x(x = C /\ x e. B)))
6		df-clel 1099	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1099	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3imtr4g 426	1 |- (A (_ B -> (C e. A -> C e. B))

Syntax hints:   -> wi 2   /\ wa 196  A.wal 672  E.wex 678   = wceq 1091   e. wcel 1092   (_ wss 1487

This theorem is referenced by:  ssel2 1503  sseli 1504  sseld 1506  reuss 1577  reupick 1578  ssconb 1598  sscon 1599  ssdif 1600  sssn 1852  prss 1854  tpss 1855  sspwb 1863  pwssun 1917  uniss 1936  unipw 1960  iunss1 2002  ss2iun 2005  ssiun 2018  poss 2129  soss 2140  onfr 2237  ssorduni 2249  onint 2261  oninton 2267  oneqmini 2272  sucssel 2321  onssneli 2349  onssneli2 2350  snsn0non 2371  ssnlim 2407  brrelex 2446  weinxp 2467  relss 2480  ssxp 2487  cnvss 2512  dmss 2530  elreldm 2554  relssres 2596  iss 2599  imasn 2616  cotr 2625  cnvsym 2626  cores 2659  funss 2682  funssres 2698  fununi 2705  funfvima2 2905  funfvima3 2906  isomin 2937  isofrlem 2939  tfrlem1 2949  tfrlem8 2956  tfrlem13 2961  tz7.48lem 2993  tz7.49 2997  nnmordi 3188  omsmolem 3195  omsmo 3196  onomeneq 3414  unblem1 3431  unblem3 3433  fiint 3445  inf3lem2 3465  r1tr 3498  tz9.13 3507  rankr1lem 3517  rankel 3524  rankval3 3525  bndrank 3526  rankpw 3528  cardlim 3657  carduni 3664  cfub 3703  suplem1pr 3955  supsr 4025  suprelem 4053  axsup 4088  sup2 4510  sup3 4511  uzwo 4605  uzwo2 4606  nnwoOLD 4608  infxpidmlem7 4939  infmap2lem1 4951  ocsh 5164  occont 5168  ococss 5174  shorth 5176  shless 5348  spansnss2t 5480  h1datom 5483  pjss2 5571  pjssm 5572  pjss1co 5633  pjorthco 5639  pj3s 5659

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