Theorem sseli 1504

Description: Membership inference from subclass relationship.

Hypothesis

Ref	Expression
sseli.1	|- A (_ B

Assertion

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

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 |- A (_ B
2		ssel 1502	. 2 |- (A (_ B -> (C e. A -> C e. B))
3	1, 2	ax-mp 6	1 |- (C e. A -> C e. B)

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

This theorem is referenced by:  sselii 1505  elun1 1625  elun2 1626  onfr 2237  nnont 2379  finds 2397  finds2 2399  brelg 2458  2elresin 2733  tz7.44-3 2968  zfregs 3491  tz9.12lem3 3505  cplem1 3545  kmlem1 3580  zornlem3 3605  zornlem4 3606  zornlem5 3607  hta 3619  pinn 3800  recnt 4097  nnret 4427  nncnt 4428  nnind 4434  nnnn0t 4541  nn0ret 4542  nn0cnt 4543  nnzt 4579  nn0zt 4580  znegclt 4588  uzwo 4605  nnqt 4638  qcnt 4639  om2uzlt 4654  om2uzf1o 4656  expcllem 4682  shel 5120  chsh 5131  chel 5137  occl 5188  choc1 5292  shintcl 5294  chintcl 5296  shslej 5339  osumlem2 5531  osumlem4 5533  pjocin 5583  pjin 5584  atelch 5742

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