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

Theorem sb6 2089
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 2479). Theorem sb6f 2497 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2475 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2069. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2155. (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 2069 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 equequ2 2030 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
32imbi1d 342 . . . 4 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
43albidv 1924 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
54equsalvw 2008 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑥(𝑥 = 𝑡𝜑))
61, 5bitri 275 1 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069
This theorem is referenced by:  2sb6  2090  sb1v  2091  sbrimvw  2095  sbievw  2096  sbcom3vv  2099  nfs1v  2154  sb4av  2237  sb6a  2250  sb5  2268  sb56OLD  2270  sbiev  2309  sb8v  2349  sb8f  2350  2eu6  2653  nfabdw  2927  nfabdwOLD  2928  elab6g  3658  ab0OLD  4374  disj  4446  iota4  6521  bj-ax12ssb  35473  bj-sbievwd  35598  bj-hbs1  35628  bj-hbsb2av  35630  bj-sbievw1  35662  bj-sbievw2  35663  bj-sbievw  35664  wl-lem-moexsb  36371  absnsb  45672  ichnfimlem  46066
  Copyright terms: Public domain W3C validator