Theorem ssel2 2067

Description: Membership relationships follow from a subclass relationship.

Assertion

Ref	Expression
ssel2	⊢ ((A ⊆ B ⋀ C ∈ A) → C ∈ B)

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 2066	. 2 ⊢ (A ⊆ B → (C ∈ A → C ∈ B))
2	1	imp 350	1 ⊢ ((A ⊆ B ⋀ C ∈ A) → C ∈ B)

Syntax hints:   → wi 3   ⋀ wa 223   ∈ wcel 960   ⊆ wss 2050

This theorem is referenced by:  tz7.7 2979  onnmin 3021  onmindif 3066  onmindif2 3067  ordunisssuc 3089  limsssuc 3127  ssimaex 3774  1st2nd 4114  fundmen 4434  isfinite2 4557  isfinite2OLD 4558  suplem2pr 5174  axsup 5519  lbinfm 6050  suprleub 6061  dfinfmr 6069  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  supxr2 6084  supxrre 6085  supxrun 6087  supxrunb1 6091  supxrbnd 6093  supxrbnd1 6097  supxrbnd2 6098  supxrub 6100  supxrleub 6101  uzwo4OLD 6212  shftf 6352  uzwo 6456  uzwoOLD 6457  sumeqfv 6997  infxpidmlem5 7557  infxpidmlem7 7559  infxpidmlem8 7560  tgclt 7623  fctopOLD 7647  cctop 7649  neips 7724  isopn4 7859  opni3 7863  opnuni 7865  lpbl 7877  metcnplem 7883  metelcls 7962  ubthlem11 8535  ocsh 9151  ocorth 9159  spansncv 9592  pjss1co 10086  sumdmdi 10337  efilcp 10556  efilcp2 10561

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 2054  df-ss 2056

Copyright terms: Public domain