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

Theorem sb6 2080
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 2472). Theorem sb6f 2490 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2468 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2060. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2146. (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 2060 . 2 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 equequ2 2021 . . . . 5 (𝑦 = 𝑡 → (𝑥 = 𝑦𝑥 = 𝑡))
32imbi1d 340 . . . 4 (𝑦 = 𝑡 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑡𝜑)))
43albidv 1915 . . 3 (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑡𝜑)))
54equsalvw 1999 . 2 (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦𝜑)) ↔ ∀𝑥(𝑥 = 𝑡𝜑))
61, 5bitri 274 1 ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  [wsb 2059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060
This theorem is referenced by:  2sb6  2081  sb1v  2082  sbrimvw  2086  sbievw  2087  sbcom3vv  2090  nfs1v  2145  sb4av  2231  sb6a  2244  sb5  2262  sb56OLD  2264  sbiev  2303  sb8v  2342  sb8f  2343  2eu6  2645  nfabdw  2915  nfabdwOLD  2916  elab6g  3655  ab0OLD  4379  disj  4451  iota4  6534  bj-ax12ssb  36322  bj-sbievwd  36447  bj-hbs1  36477  bj-hbsb2av  36479  bj-sbievw1  36510  bj-sbievw2  36511  bj-sbievw  36512  wl-sbid2ft  37200  wl-sb9v  37204  wl-lem-moexsb  37223  absnsb  46591  ichnfimlem  46984
  Copyright terms: Public domain W3C validator