Theorem sbequ 2376

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 2375	. 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2		sbequi 2375	. . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
3	2	equcoms 1947	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
4	1, 3	impbid 202	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Syntax hints:   → wi 4   ↔ wb 196  [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  drsb2  2378  sbcom3  2411  sbco2  2415  sbcom2  2445  sb10f  2456  sb8eu  2503  cbvralf  3165  cbvreu  3169  cbvralsv  3182  cbvrexsv  3183  cbvrab  3198  cbvreucsf  3567  cbvrabcsf  3568  sbss  4084  cbvopab1  4723  cbvmpt  4749  cbviota  5856  sb8iota  5858  cbvriota  6621  tfis  7054  tfinds  7059  findes  7096  uzind4s  11748  bj-cleljustab  32847  wl-sbcom2d-lem1  33342  wl-sb8eut  33359  wl-sbcom3  33372  sbeqi  33968  disjinfi  39380