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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  [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 1911  ax-6 1969  ax-7 2009

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbequi  2085  sbcom3vv  2096  sbco2vv  2098  sbcom2  2159  drsb2  2255  sbco2v  2324  sbcom3  2503  sbco2  2508  sb10f  2524  sb8eulem  2590  eleq1ab  2709  cbvralsvwOLD  3314  cbvrexsvwOLD  3315  cbvralfwOLD  3318  cbvralf  3354  cbvralsv  3360  cbvrexsv  3361  cbvreuwOLD  3410  cbvreu  3422  cbvrabw  3465  cbvrab  3471  cbvreucsf  3941  cbvrabcsf  3942  ss2abdv  4061  cbvopab1g  5225  cbvmptf  5258  cbvmptfg  5259  cbviota  6506  sb8iota  6508  cbvriota  7383  tfis  7848  tfinds  7853  findes  7897  uzind4s  12898  wl-sbcom2d-lem1  36729  wl-sb8eut  36747  wl-dfclab  36763  sbeqi  37332  disjinfi  44191  2reu8i  46121