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

Step	Hyp	Ref	Expression
1		sbequi 2258	. 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2		sbequi 2258	. . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
3	2	equcoms 1896	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
4	1, 3	impbid 197	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

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