Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssel2 GIF version

Theorem ssel2 3092
 Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
Assertion
Ref Expression
ssel2 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)

Proof of Theorem ssel2
StepHypRef Expression
1 ssel 3091 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
21imp 123 1 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480   ⊆ wss 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084 This theorem is referenced by:  elnn  4519  funimass4  5472  fvelimab  5477  ssimaex  5482  funconstss  5538  rexima  5656  ralima  5657  1st2nd  6079  f1o2ndf1  6125  tfri1dALT  6248  eldju1st  6956  axsuploc  7844  lbinf  8713  dfinfre  8721  lbzbi  9415  elfzom1elp1fzo  9986  ssfzo12  10008  seq3split  10259  shftlem  10595  tgcl  12243  neipsm  12333  txbasval  12446  elmopn2  12628  metrest  12685  cncfmet  12758  negcncf  12767  reeff1olem  12870
 Copyright terms: Public domain W3C validator