sbcom2

Description: Commutativity law for substitution. Used in proof of Theorem 9.7 of Megill p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997) (Proof shortened by Wolf Lammen, 23-Dec-2022)

		Ref	Expression
	Assertion	sbcom2	$⊢ [w/ z] [y/ x] φ \leftrightarrow [y/ x] [w/ z] φ$

Proof

Step	Hyp	Ref	Expression
1		2sb6	$⊢ [v/ z] [u/ x] φ \leftrightarrow \forall z \forall x ((z = v \land x = u) \to φ)$
2		alcom	$⊢ \forall z \forall x ((z = v \land x = u) \to φ) \leftrightarrow \forall x \forall z ((z = v \land x = u) \to φ)$
3		ancomst	$⊢ ((z = v \land x = u) \to φ) \leftrightarrow ((x = u \land z = v) \to φ)$
4	3	2albii	$⊢ \forall x \forall z ((z = v \land x = u) \to φ) \leftrightarrow \forall x \forall z ((x = u \land z = v) \to φ)$
5	1 2 4	3bitri	$⊢ [v/ z] [u/ x] φ \leftrightarrow \forall x \forall z ((x = u \land z = v) \to φ)$
6		2sb6	$⊢ [u/ x] [v/ z] φ \leftrightarrow \forall x \forall z ((x = u \land z = v) \to φ)$
7	5 6	bitr4i	$⊢ [v/ z] [u/ x] φ \leftrightarrow [u/ x] [v/ z] φ$
8		sbequ	$⊢ u = y \to ([u/ x] φ \leftrightarrow [y/ x] φ)$
9	8	sbbidv	$⊢ u = y \to ([v/ z] [u/ x] φ \leftrightarrow [v/ z] [y/ x] φ)$
10	7 9	bitr3id	$⊢ u = y \to ([u/ x] [v/ z] φ \leftrightarrow [v/ z] [y/ x] φ)$
11		sbequ	$⊢ v = w \to ([v/ z] [y/ x] φ \leftrightarrow [w/ z] [y/ x] φ)$
12	10 11	sylan9bb	$⊢ (u = y \land v = w) \to ([u/ x] [v/ z] φ \leftrightarrow [w/ z] [y/ x] φ)$
13		sbequ	$⊢ v = w \to ([v/ z] φ \leftrightarrow [w/ z] φ)$
14	13	sbbidv	$⊢ v = w \to ([u/ x] [v/ z] φ \leftrightarrow [u/ x] [w/ z] φ)$
15		sbequ	$⊢ u = y \to ([u/ x] [w/ z] φ \leftrightarrow [y/ x] [w/ z] φ)$
16	14 15	sylan9bbr	$⊢ (u = y \land v = w) \to ([u/ x] [v/ z] φ \leftrightarrow [y/ x] [w/ z] φ)$
17	12 16	bitr3d	$⊢ (u = y \land v = w) \to ([w/ z] [y/ x] φ \leftrightarrow [y/ x] [w/ z] φ)$
18	17	ex	$⊢ u = y \to (v = w \to ([w/ z] [y/ x] φ \leftrightarrow [y/ x] [w/ z] φ))$
19		ax6ev	$⊢ \exists u u = y$
20	18 19	exlimiiv	$⊢ v = w \to ([w/ z] [y/ x] φ \leftrightarrow [y/ x] [w/ z] φ)$
21		ax6ev	$⊢ \exists v v = w$
22	20 21	exlimiiv	$⊢ [w/ z] [y/ x] φ \leftrightarrow [y/ x] [w/ z] φ$

Metamath Proof Explorer

Theorem sbcom2

Proof