Theorem sbequ 2380

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-10 2021  ax-12 2049  ax-13 2250

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-sb 1883

This theorem is referenced by:  drsb2  2382  sbcom3  2415  sbco2  2419  sbcom2  2449  sb10f  2460  sb8eu  2507  cbvralf  3158  cbvreu  3162  cbvralsv  3175  cbvrexsv  3176  cbvrab  3189  cbvreucsf  3553  cbvrabcsf  3554  sbss  4061  cbvopab1  4690  cbvmpt  4714  cbviota  5818  sb8iota  5820  cbvriota  6576  tfis  7002  tfinds  7007  findes  7044  uzind4s  11692  bj-cleljustab  32465  wl-sbcom2d-lem1  32950  wl-sb8eut  32967  wl-sbcom3  32980  sbeqi  33567  disjinfi  38821