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

Theorem sb4b 2488
 Description: Simplified definition of substitution when variables are distinct. Version of sb6 2090 with a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 27-May-1997.) Revise df-sb 2070. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
Assertion
Ref Expression
sb4b (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑)))

Proof of Theorem sb4b
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nfna1 2153 . . . . . 6 𝑥 ¬ ∀𝑥 𝑥 = 𝑡
2 nfeqf2 2384 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑡 → Ⅎ𝑥 𝑦 = 𝑡)
31, 2nfan1 2198 . . . . 5 𝑥(¬ ∀𝑥 𝑥 = 𝑡𝑦 = 𝑡)
4 equequ2 2033 . . . . . . 7 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
54imbi1d 345 . . . . . 6 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
65adantl 485 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑡𝑦 = 𝑡) → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
73, 6albid 2222 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑡𝑦 = 𝑡) → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
87pm5.74da 803 . . 3 (¬ ∀𝑥 𝑥 = 𝑡 → ((𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡𝜑))))
98albidv 1921 . 2 (¬ ∀𝑥 𝑥 = 𝑡 → (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡𝜑))))
10 df-sb 2070 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
11 ax6ev 1972 . . . 4 𝑦 𝑦 = 𝑡
1211a1bi 366 . . 3 (∀𝑥(𝑥 = 𝑡𝜑) ↔ (∃𝑦 𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡𝜑)))
13 19.23v 1943 . . 3 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ (∃𝑦 𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡𝜑)))
1412, 13bitr4i 281 . 2 (∀𝑥(𝑥 = 𝑡𝜑) ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑡𝜑)))
159, 10, 143bitr4g 317 1 (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781  [wsb 2069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-12 2175  ax-13 2379 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070 This theorem is referenced by:  sb3b  2490  sb2  2493  sb4OLD  2495  sb1OLD  2496  sb4a  2498  hbsb2  2500  dfsb2  2511  sbcom3  2525  sbal1  2548  sbal2  2549  sbal2OLD  2550  wl-2sb6d  34978  wl-sbalnae  34982
 Copyright terms: Public domain W3C validator