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

Theorem sb6 2084
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 2497). Theorem sb6f 2530 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2492 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2151. (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 2061 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 equequ2 2024 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
32imbi1d 343 . . . 4 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
43albidv 1912 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
54equsalvw 2001 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑥(𝑥 = 𝑡𝜑))
61, 5bitri 276 1 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061
This theorem is referenced by:  2sb6  2085  sb1v  2086  sb4vOLD  2087  sb2vOLD  2088  sbrimvlem  2092  sbievw  2094  sbcom3vv  2097  sb4av  2234  sb6a  2249  nfs1v  2264  sb56  2268  sb5OLD  2272  sbnvOLD  2313  sbiev  2321  sbequivvOLD  2325  nfsbvOLD  2341  2eu6  2737  nfabdw  2997  iota4  6329  bj-ax12ssb  33888  bj-hbs1  34031  bj-hbsb2av  34033  bj-sbievw1  34066  bj-sbievw2  34067  bj-sbievw  34068  wl-lem-moexsb  34685  wl-dfralsb  34718  wl-dfrabsb  34742  absnsb  43139
  Copyright terms: Public domain W3C validator