Theorem sbequ 2093

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 2075. (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 2038	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦))
2	1	imbi1d 345	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
3	2	albidv 1927	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
4		df-sb 2075	. 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
5		df-sb 2075	. 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1540  [wsb 2074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075

This theorem is referenced by:  sbequi  2094  sbcom3vv  2106  sbco2vv  2108  sbcom2  2169  drsb2  2267  sbco2v  2334  sbcom3  2510  sbco2  2515  sb10f  2532  sb8eulem  2599  eleq1ab  2718  cbvralfwOLD  3336  cbvralf  3338  cbvreuw  3342  cbvreu  3347  cbvralsvw  3368  cbvrexsvw  3369  cbvralsv  3370  cbvrexsv  3371  cbvrabw  3391  cbvrab  3392  cbvreucsf  3834  cbvrabcsf  3835  ss2abdv  3953  cbvopab1g  5104  cbvmptf  5129  cbvmptfg  5130  cbviota  6307  sb8iota  6309  cbvriota  7141  tfis  7588  tfinds  7593  findes  7633  uzind4s  12390  wl-sbcom2d-lem1  35337  wl-sb8eut  35355  wl-dfclab  35370  sbeqi  35940  disjinfi  42269  2reu8i  44138