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

Theorem sb6 2090
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 2493). Theorem sb6f 2515 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2488 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2070. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2158. (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 2070 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 equequ2 2033 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
32imbi1d 345 . . . 4 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
43albidv 1921 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
54equsalvw 2010 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑥(𝑥 = 𝑡𝜑))
61, 5bitri 278 1 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1536  [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
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070
This theorem is referenced by:  2sb6  2091  sb1v  2092  sb4vOLD  2093  sb2vOLD  2094  sbrimvlem  2098  sbievw  2100  sbcom3vv  2103  nfs1v  2157  sb4av  2242  sb6a  2256  sb56  2274  sb5OLD  2277  sbiev  2322  nfsbvOLD  2339  2eu6  2719  nfabdw  2976  disj  4355  iota4  6305  bj-ax12ssb  34104  bj-hbs1  34249  bj-hbsb2av  34251  bj-sbievw1  34284  bj-sbievw2  34285  bj-sbievw  34286  wl-lem-moexsb  34969  wl-dfralsb  35002  wl-dfrabsb  35026  absnsb  43617  ichnfimlem  43978
  Copyright terms: Public domain W3C validator