Theorem sbequ 2085

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1538  [wsb 2066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067

This theorem is referenced by:  sbequi  2086  sbcom3vv  2097  sbco2vv  2099  sbcom2  2160  drsb2  2256  sbco2v  2325  sbcom3  2504  sbco2  2509  sb10f  2525  sb8eulem  2591  eleq1ab  2710  cbvralsvwOLD  3315  cbvrexsvwOLD  3316  cbvralfwOLD  3319  cbvralf  3355  cbvralsv  3361  cbvrexsv  3362  cbvreuwOLD  3411  cbvreu  3423  cbvrabw  3466  cbvrab  3472  cbvreucsf  3940  cbvrabcsf  3941  ss2abdv  4060  cbvopab1g  5224  cbvmptf  5257  cbvmptfg  5258  cbviota  6505  sb8iota  6507  cbvriota  7382  tfis  7848  tfinds  7853  findes  7897  uzind4s  12899  wl-sbcom2d-lem1  36887  wl-sb8eut  36905  wl-dfclab  36921  sbeqi  37490  disjinfi  44349  2reu8i  46279