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

Theorem sbequ 2089
Description: Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.) Revise df-sb 2069. (Revised by BJ, 30-Dec-2020.)
Assertion
Ref Expression
sbequ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 equequ2 2032 . . . 4 (𝑥 = 𝑦 → (𝑢 = 𝑥𝑢 = 𝑦))
21imbi1d 344 . . 3 (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑))))
32albidv 1920 . 2 (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑))))
4 df-sb 2069 . 2 ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)))
5 df-sb 2069 . 2 ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑)))
63, 4, 53bitr4g 316 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wal 1534  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069
This theorem is referenced by:  sbequi  2090  sbcom3vv  2105  sbco2vv  2107  sbcom2  2167  drsb2  2266  sbco2v  2351  sbcom3  2547  sbco2  2552  sb10f  2570  sb8eulem  2683  eleq1ab  2804  cbvralfw  3440  cbvralf  3442  cbvreuw  3446  cbvreu  3450  cbvralsvw  3470  cbvrexsvw  3471  cbvralsv  3472  cbvrexsv  3473  cbvrabw  3492  cbvrab  3493  cbvreucsf  3930  cbvrabcsf  3931  cbvopab1g  5143  cbvmptf  5168  cbvmptfg  5169  cbviota  6326  sb8iota  6328  cbvriota  7130  tfis  7572  tfinds  7577  findes  7615  uzind4s  12311  wl-sbcom2d-lem1  34799  wl-sb8eut  34817  wl-dfclab  34832  sbeqi  35441  disjinfi  41460  2reu8i  43319
  Copyright terms: Public domain W3C validator