Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ax12ssb Structured version   Visualization version   GIF version

Theorem bj-ax12ssb 34386
 Description: Axiom bj-ax12 34385 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ax12ssb [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
Distinct variable group:   𝑥,𝑡
Allowed substitution hints:   𝜑(𝑥,𝑡)

Proof of Theorem bj-ax12ssb
StepHypRef Expression
1 bj-ax12 34385 . . 3 𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑)))
2 sb6 2091 . . . . . 6 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
32imbi2i 340 . . . . 5 ((𝜑 → [𝑡 / 𝑥]𝜑) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑)))
43imbi2i 340 . . . 4 ((𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
54albii 1822 . . 3 (∀𝑥(𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
61, 5mpbir 234 . 2 𝑥(𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑))
7 sb6 2091 . 2 ([𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)))
86, 7mpbir 234 1 [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1537  [wsb 2070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-12 2176 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator