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

Theorem sstr2 3032
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
sstr2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))

Proof of Theorem sstr2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ssel 3019 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 74 . . 3 (𝐴𝐵 → ((𝑥𝐵𝑥𝐶) → (𝑥𝐴𝑥𝐶)))
32alimdv 1807 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝑥𝐶) → ∀𝑥(𝑥𝐴𝑥𝐶)))
4 dfss2 3014 . 2 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
5 dfss2 3014 . 2 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
63, 4, 53imtr4g 203 1 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287  wcel 1438  wss 2999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3005  df-ss 3012
This theorem is referenced by:  sstr  3033  sstri  3034  sseq1  3047  sseq2  3048  ssun3  3165  ssun4  3166  ssinss1  3228  ssdisj  3339  triun  3949  trintssm  3952  sspwb  4043  exss  4054  relss  4525  funss  5034  funimass2  5092  fss  5172  fiintim  6637  sbthlem2  6665  sbthlemi3  6666  sbthlemi6  6669  bj-nntrans  11801
  Copyright terms: Public domain W3C validator