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

Theorem bj-ssb0 32323
Description: Substitution for a variable not occurring in a proposition. See sbf 2379. (Contributed by BJ, 22-Dec-2020.)
Assertion
Ref Expression
bj-ssb0 ([𝑡/𝑥]b𝜑𝜑)
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜑(𝑡)

Proof of Theorem bj-ssb0
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-ssb 32315 . 2 ([𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 19.23v 1899 . . . . . . 7 (∀𝑥(𝑥 = 𝑦𝜑) ↔ (∃𝑥 𝑥 = 𝑦𝜑))
3 ax6ev 1887 . . . . . . . . 9 𝑥 𝑥 = 𝑦
4 pm2.27 42 . . . . . . . . 9 (∃𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑦𝜑) → 𝜑))
53, 4ax-mp 5 . . . . . . . 8 ((∃𝑥 𝑥 = 𝑦𝜑) → 𝜑)
6 ax-1 6 . . . . . . . 8 (𝜑 → (∃𝑥 𝑥 = 𝑦𝜑))
75, 6impbii 199 . . . . . . 7 ((∃𝑥 𝑥 = 𝑦𝜑) ↔ 𝜑)
82, 7bitri 264 . . . . . 6 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜑)
98imbi2i 326 . . . . 5 ((𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ (𝑦 = 𝑡𝜑))
109albii 1744 . . . 4 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑦(𝑦 = 𝑡𝜑))
11 19.23v 1899 . . . 4 (∀𝑦(𝑦 = 𝑡𝜑) ↔ (∃𝑦 𝑦 = 𝑡𝜑))
1210, 11bitri 264 . . 3 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ (∃𝑦 𝑦 = 𝑡𝜑))
13 ax6ev 1887 . . . . 5 𝑦 𝑦 = 𝑡
14 pm2.27 42 . . . . 5 (∃𝑦 𝑦 = 𝑡 → ((∃𝑦 𝑦 = 𝑡𝜑) → 𝜑))
1513, 14ax-mp 5 . . . 4 ((∃𝑦 𝑦 = 𝑡𝜑) → 𝜑)
16 ax-1 6 . . . 4 (𝜑 → (∃𝑦 𝑦 = 𝑡𝜑))
1715, 16impbii 199 . . 3 ((∃𝑦 𝑦 = 𝑡𝜑) ↔ 𝜑)
1812, 17bitri 264 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ 𝜑)
191, 18bitri 264 1 ([𝑡/𝑥]b𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478  wex 1701  [wssb 32314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-ssb 32315
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator