Theorem sbequ 2122

Description: Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.) Revise df-sb 2102. (Revised by BJ, 30-Dec-2020.)

Assertion

Ref	Expression
sbequ	⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ

Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 2061	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦))
2	1	imbi1d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
3	2	albidv 1955	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
4		dfsb 2103	. 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
5		dfsb 2103	. 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  [wsb 2101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102

This theorem is used by:  sbequiOLD  2123  sbcom3vv  2136  sbco2vv  2138  sbco4lem  2140  sbco4  2141  sbcom2  2212  drsb2  2304  sbco2v  2365  sbcom3  2538  sbco2  2543  sb10f  2559  sb8eulem  2626  eleq1ab  2743  cbvralf  3349  cbvralsv  3355  cbvrexsv  3356  cbvreu  3408  cbvrab  3453  cbvreucsf  3895  cbvrabcsf  3896  cbvopab1g  5186  cbvmptfg  5212  cbviota  6529  sb8iota  6531  cbvriota  7421  tfis  7900  tfinds  7905  findes  7946  uzind4s  13075  regsfromregtco  37541  bj-axseprep  38260  wl-sbcom2d-lem1  38759  wl-sb8eut  38778  wl-sb8eutv  38779  wl-dfclab  38785  sbeqi  39357  disjinfi  46480  2reu8i  48457