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 2483). Theorem sb6f 2501 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2479 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2064. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2156. (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 2064 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 equequ2 2024 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
32imbi1d 341 . . . 4 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
43albidv 1919 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
54equsalvw 2002 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑥(𝑥 = 𝑡𝜑))
61, 5bitri 275 1 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1537  [wsb 2063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064
This theorem is referenced by:  2sb6  2085  sb1v  2086  sbrimvw  2090  sbbiiev  2091  sbievwOLD  2093  nfs1v  2155  sb4av  2243  sb6a  2257  sb5  2275  sbievOLD  2314  sb8v  2354  sb8f  2355  2eu6  2656  nfabdw  2926  elab6g  3668  disj  4449  iota4  6541  in-ax8  36226  bj-ax12ssb  36660  bj-sbievwd  36784  bj-hbs1  36814  bj-hbsb2av  36816  bj-sbievw1  36847  bj-sbievw2  36848  bj-sbievw  36849  wl-sbid2ft  37547  wl-sb9v  37551  wl-lem-moexsb  37570  absnsb  47044  ichnfimlem  47455
  Copyright terms: Public domain W3C validator