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

Theorem sbequ 2259
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 2258 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 2258 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1896 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 197 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  [wsb 1828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 192  df-an 380  df-ex 1693  df-nf 1697  df-sb 1829
This theorem is referenced by:  drsb2  2261  sbcom3  2294  sbco2  2298  sbcom2  2328  sb10f  2339  sb8eu  2386  cbvralf  3034  cbvreu  3038  cbvralsv  3051  cbvrexsv  3052  cbvrab  3064  cbvreucsf  3419  cbvrabcsf  3420  sbss  3906  cbvopab1  4505  cbvmpt  4527  cbviota  5602  sb8iota  5604  cbvriota  6335  tfis  6758  tfinds  6763  findes  6800  uzind4s  11309  wl-sbcom2d-lem1  32120  wl-sb8eut  32137  wl-sbcom3  32150  sbeqi  32639  disjinfi  37828
  Copyright terms: Public domain W3C validator