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

Theorem sbequ 2523
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 2522 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 2522 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 2105 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 202 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  [wsb 2049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-ex 1853  df-nf 1858  df-sb 2050
This theorem is referenced by:  drsb2  2525  sbcom3  2558  sbco2  2562  sbcom2  2593  sb10f  2604  sb8eu  2652  cbvralf  3314  cbvreu  3318  cbvralsv  3331  cbvrexsv  3332  cbvrab  3348  cbvreucsf  3717  cbvrabcsf  3718  sbss  4224  cbvopab1  4858  cbvmpt  4884  cbviota  6000  sb8iota  6002  cbvriota  6765  tfis  7202  tfinds  7207  findes  7244  uzind4s  11951  bj-cleljustab  33182  wl-sbcom2d-lem1  33677  wl-sb8eut  33694  sbeqi  34301  disjinfi  39901
  Copyright terms: Public domain W3C validator