Theorem sbequ 2123

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 2098. (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 2053	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦))
2	1	imbi1d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
3	2	albidv 1947	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
4		dfsb 2100	. 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
5		dfsb 2100	. 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565  [wsb 2097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098

This theorem is referenced by:  sbequi  2124  sbcom3vv  2138  sbco2vv  2140  sbco4lem  2142  sbco4  2143  sbcom2  2213  drsb2  2308  sbco2v  2370  sbcom3  2544  sbco2  2549  sb10f  2565  sb8eulem  2632  eleq1ab  2749  cbvralf  3356  cbvralsv  3362  cbvrexsv  3363  cbvreu  3415  cbvrabwOLD  3459  cbvrab  3462  cbvreucsf  3905  cbvrabcsf  3906  cbvopab1g  5190  cbvmptfg  5216  cbviota  6502  sb8iota  6504  cbvriota  7381  tfis  7850  tfinds  7855  findes  7896  uzind4s  12931  regsfromregtco  36937  wl-sbcom2d-lem1  38101  wl-sb8eut  38120  wl-sb8eutv  38121  wl-dfclab  38127  sbeqi  38697  disjinfi  45801  2reu8i  47738