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

Theorem sbequ 2452
Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sbequ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 2451 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 2451 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 2067 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 204 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  [wsb 2011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-12 2163  ax-13 2334
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-sb 2012
This theorem is referenced by:  drsb2  2454  sbcom3  2487  sbco2  2492  sbcom2  2523  sbcom2OLD  2524  sb10f  2536  sb8eu  2635  cbvralf  3361  cbvreu  3365  cbvralsv  3378  cbvrexsv  3379  cbvrab  3395  cbvreucsf  3785  cbvrabcsf  3786  sbss  4305  cbvopab1  4959  cbvmpt  4984  cbviota  6104  sb8iota  6106  cbvriota  6893  tfis  7332  tfinds  7337  findes  7374  uzind4s  12054  bj-cleljustab  33422  wl-sbcom2d-lem1  33936  wl-sb8eut  33953  sbeqi  34590  cleljust2  38121  disjinfi  40303  2reu8i  42154
  Copyright terms: Public domain W3C validator