Theorem ssel2 2062

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 2061	. 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 957   (_ wss 2045

This theorem is referenced by:  tz7.7 2970  onnmin 3012  onmindif 3057  onmindif2 3058  ordunisssuc 3080  limsssuc 3118  ssimaex 3765  1st2nd 4105  fundmen 4422  isfinite2 4536  suplem2pr 5149  axsup 5494  lbinfm 6009  suprleub 6020  dfinfmr 6028  infmrcl 6030  xrsupsslem 6037  xrinfmsslem 6038  xrub 6041  supxr2 6043  supxrre 6044  supxrun 6046  supxrunb1 6050  supxrbnd 6052  supxrbnd1 6056  supxrbnd2 6057  supxrub 6059  supxrleub 6060  uzwo4OLD 6172  shftf 6306  uzwo 6405  uzwoOLD 6406  sumeqfv 6965  infxpidmlem5 7535  infxpidmlem7 7537  infxpidmlem8 7538  tgclt 7603  fctop 7629  cctop 7631  neips 7706  isopn4 7845  opni3 7849  opnuni 7851  lpbl 7863  metcnplem 7869  metelcls 7948  ubthlem11 8523  ocsh 9144  ocorth 9152  spansncv 9587  spansncvOLD 9588  pjss1co 10082  sumdmdi 10333  efilcp 10539  efilcp2 10544

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2049  df-ss 2051

Copyright terms: Public domain