Theorem ssel2 2060

Description: Membership relationships follow from a subclass relationship.

Assertion

Ref	Expression
ssel2	|- ((A (_ B /\ C e. A) -> C e. B)

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 2059	. 2 |- (A (_ B -> (C e. A -> C e. B))
2	1	imp 350	1 |- ((A (_ B /\ C e. A) -> C e. B)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 956   (_ wss 2043

This theorem is referenced by:  tz7.7 2968  onnmin 3010  onmindif 3055  onmindif2 3056  ordunisssuc 3078  limsssuc 3116  ssimaex 3759  1st2nd 4098  fundmen 4415  isfinite2 4529  suplem2pr 5142  axsup 5487  lbinfm 6003  suprleub 6014  dfinfmr 6022  infmrcl 6024  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxr2 6037  supxrre 6038  supxrun 6040  supxrunb1 6044  supxrbnd 6046  supxrbnd1 6050  supxrbnd2 6051  supxrub 6053  supxrleub 6054  uzwo4OLD 6166  shftf 6296  uzwo 6395  uzwoOLD 6396  sumeqfv 6943  infxpidmlem5 7507  infxpidmlem7 7509  infxpidmlem8 7510  tgclt 7574  fctop 7600  cctop 7602  neips 7677  isopn4 7814  opni3 7818  opnuni 7820  lpbl 7832  metcnplem 7838  metelcls 7916  ubthlem11 8483  ocsh 9095  ocorth 9103  spansncv 9537  pjss1co 10029  sumdmdi 10278  efilcp 10481  efilcp2 10486

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain