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

Theorem sb6 2064
 Description: Alternate definition of substitution when variables are disjoint. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left" also holds without a disjoint variable condition (sb2 2456). Theorem sb6f 2489 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2455 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2041. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2124. (Revised by Steven Nguyen, 7-Jul-2023.) (Proof shortened by Wolf Lammen, 16-Jul-2023.)
Assertion
Ref Expression
sb6 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
Distinct variable group:   𝑥,𝑡
Allowed substitution hints:   𝜑(𝑥,𝑡)

Proof of Theorem sb6
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-sb 2041 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 equequ2 2008 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
32imbi1d 343 . . . 4 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
43albidv 1896 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
54equsalvw 1985 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑥(𝑥 = 𝑡𝜑))
61, 5bitri 276 1 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1518  [wsb 2040 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-sb 2041 This theorem is referenced by:  sb4vOLD  2065  sb2vOLD  2066  sbievw  2070  sbcom3vv  2071  sb6a  2220  nfs1v  2235  sb56  2239  sb5OLD  2242  2sb6  2244  sbnvOLD  2285  sbiev  2293  sbequivvOLD  2295  nfsbvOLD  2311  2sb8evOLD  2330  2eu6  2712  iota4  6199  bj-ax12ssb  33534  bj-hbs1  33628  bj-hbsb2av  33630  bj-sbievw1  33683  bj-sbievw2  33684  bj-sbievw  33685  wl-lem-moexsb  34281  wl-dfralsb  34314  wl-dfrabsb  34338  absnsb  42732
 Copyright terms: Public domain W3C validator