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

Theorem sbequ 2268
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 2267 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 2267 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1897 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 200 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  [wsb 1830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1699  df-sb 1831
This theorem is referenced by:  drsb2  2270  sbcom3  2303  sbco2  2307  sbcom2  2337  sb10f  2348  sb8eu  2395  cbvralf  3045  cbvreu  3049  cbvralsv  3062  cbvrexsv  3063  cbvrab  3075  cbvreucsf  3437  cbvrabcsf  3438  sbss  3937  cbvopab1  4553  cbvmpt  4575  cbviota  5663  sb8iota  5665  cbvriota  6403  tfis  6827  tfinds  6832  findes  6869  uzind4s  11492  wl-sbcom2d-lem1  32415  wl-sb8eut  32432  wl-sbcom3  32445  sbeqi  33032  disjinfi  38277
  Copyright terms: Public domain W3C validator