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

Theorem sselda 2973
Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
Hypothesis
Ref Expression
sseld.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
sselda ((𝜑𝐶𝐴) → 𝐶𝐵)

Proof of Theorem sselda
StepHypRef Expression
1 sseld.1 . . 3 (𝜑𝐴𝐵)
21sseld 2972 . 2 (𝜑 → (𝐶𝐴𝐶𝐵))
32imp 119 1 ((𝜑𝐶𝐴) → 𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wcel 1409  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  elrel  4470  ffvresb  5356  1stdm  5836  tfrlem1  5954  tfrlemiubacc  5975  erinxp  6211  fundmen  6317  supisolem  6412  ordiso2  6415  elprnql  6637  elprnqu  6638  un0addcl  8272  un0mulcl  8273  icoshftf1o  8960  elfzom1elfzo  9161  zpnn0elfzo  9165  iseqfveq  9394  monoord2  9400
  Copyright terms: Public domain W3C validator