Theorem sbequ 2087

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069

This theorem is referenced by:  sbequi  2088  sbcom3vv  2099  sbco2vv  2101  sbcom2  2162  drsb2  2258  sbco2v  2327  sbcom3  2506  sbco2  2511  sb10f  2527  sb8eulem  2593  eleq1ab  2712  cbvralsvwOLD  3317  cbvrexsvwOLD  3318  cbvralfwOLD  3321  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvreuwOLD  3413  cbvreu  3425  cbvrabw  3468  cbvrab  3474  cbvreucsf  3940  cbvrabcsf  3941  ss2abdv  4060  cbvopab1g  5224  cbvmptf  5257  cbvmptfg  5258  cbviota  6503  sb8iota  6505  cbvriota  7376  tfis  7841  tfinds  7846  findes  7890  uzind4s  12889  wl-sbcom2d-lem1  36413  wl-sb8eut  36431  wl-dfclab  36447  sbeqi  37016  disjinfi  43877  2reu8i  45808