Theorem ssel2 2068

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 2067	. 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 960   (_ wss 2051

This theorem is referenced by:  tz7.7 2980  onnmin 3022  onmindif 3067  onmindif2 3068  ordunisssuc 3090  limsssuc 3128  ssimaex 3775  1st2nd 4115  fundmen 4435  isfinite2 4559  isfinite2OLD 4560  suplem2pr 5181  axsup 5526  lbinfm 6057  suprleub 6068  dfinfmr 6076  infmrcl 6078  xrsupsslem 6085  xrinfmsslem 6086  xrub 6089  supxr2 6091  supxrre 6092  supxrun 6094  supxrunb1 6098  supxrbnd 6100  supxrbnd1 6104  supxrbnd2 6105  supxrub 6107  supxrleub 6108  uzwo4OLD 6219  shftf 6359  uzwo 6463  uzwoOLD 6464  sumeqfv 7004  infxpidmlem5 7564  infxpidmlem7 7566  infxpidmlem8 7567  tgclt 7630  fctopOLD 7654  cctop 7656  neips 7731  isopn4 7866  opni3 7870  opnuni 7872  lpbl 7884  metcnplem 7890  metelcls 7969  ubthlem11 8542  ocsh 9158  ocorth 9166  spansncv 9599  pjss1co 10093  sumdmdi 10345  efilcp 10564  efilcp2 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2055  df-ss 2057

Copyright terms: Public domain