Theorem sbequ 2084

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbequi  2085  sbcom3vv  2098  sbco2vv  2100  sbco4lem  2102  sbco4  2103  sbcom2  2174  drsb2  2267  sbco2v  2330  sbcom3  2505  sbco2  2510  sb10f  2526  sb8eulem  2592  eleq1ab  2710  cbvralsvwOLDOLD  3295  cbvrexsvwOLD  3296  cbvralf  3336  cbvralsv  3342  cbvrexsv  3343  cbvreuwOLD  3389  cbvreu  3400  cbvrabwOLD  3445  cbvrab  3449  cbvreucsf  3909  cbvrabcsf  3910  cbvopab1g  5185  cbvmptf  5210  cbvmptfg  5211  cbviota  6476  sb8iota  6478  cbvriota  7360  tfis  7834  tfinds  7839  findes  7879  uzind4s  12874  wl-sbcom2d-lem1  37554  wl-sb8eut  37573  wl-sb8eutv  37574  wl-dfclab  37591  sbeqi  38160  disjinfi  45193  2reu8i  47118