MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sstr2OLD Structured version   Visualization version   GIF version

Theorem sstr2OLD 4002
Description: Obsolete version of sstr2 4001 as of 19-May-2025. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sstr2OLD (𝐴𝐵 → (𝐵𝐶𝐴𝐶))

Proof of Theorem sstr2OLD
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ssel 3988 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . . 3 (𝐴𝐵 → ((𝑥𝐵𝑥𝐶) → (𝑥𝐴𝑥𝐶)))
32alimdv 1913 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝑥𝐶) → ∀𝑥(𝑥𝐴𝑥𝐶)))
4 df-ss 3979 . 2 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
5 df-ss 3979 . 2 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
63, 4, 53imtr4g 296 1 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1534  wcel 2105  wss 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator