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

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

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