Theorem sbequ 2080

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 2062. (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 2022	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦))
2	1	imbi1d 341	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
3	2	albidv 1917	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))))
4		df-sb 2062	. 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
5		df-sb 2062	. 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534  [wsb 2061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062

This theorem is referenced by:  sbequi  2081  sbcom3vv  2094  sbco2vv  2096  sbco4lem  2098  sbco4  2099  sbcom2  2170  drsb2  2263  sbco2v  2330  sbcom3  2508  sbco2  2513  sb10f  2529  sb8eulem  2595  eleq1ab  2713  cbvralsvwOLDOLD  3317  cbvrexsvwOLD  3318  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvreuwOLD  3412  cbvreu  3424  cbvrabwOLD  3471  cbvrab  3476  cbvreucsf  3954  cbvrabcsf  3955  cbvopab1g  5223  cbvmptf  5256  cbvmptfg  5257  cbviota  6524  sb8iota  6526  cbvriota  7400  tfis  7875  tfinds  7880  findes  7922  uzind4s  12947  wl-sbcom2d-lem1  37539  wl-sb8eut  37558  wl-sb8eutv  37559  wl-dfclab  37576  sbeqi  38145  disjinfi  45134  2reu8i  47062