wl-sbcom2d

Description: Version of sbcom2 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019)

	Ref	Expression
Hypotheses	wl-sbcom2d.1	$⊢ φ \to \neg \forall x x = w$
	wl-sbcom2d.2	$⊢ φ \to \neg \forall x x = z$
	wl-sbcom2d.3	$⊢ φ \to \neg \forall z z = y$
Assertion	wl-sbcom2d	$⊢ φ \to ([w/ z] [y/ x] ψ \leftrightarrow [y/ x] [w/ z] ψ)$

Proof

Step	Hyp	Ref	Expression
1		wl-sbcom2d.1	$⊢ φ \to \neg \forall x x = w$
2		wl-sbcom2d.2	$⊢ φ \to \neg \forall x x = z$
3		wl-sbcom2d.3	$⊢ φ \to \neg \forall z z = y$
4		ax6ev	$⊢ \exists u u = y$
5		ax6ev	$⊢ \exists v v = w$
6		wl-sbcom2d-lem2	$⊢ \neg \forall z z = x \to ([u/ x] [v/ z] ψ \leftrightarrow \forall x \forall z ((x = u \land z = v) \to ψ))$
7		alcom	$⊢ \forall x \forall z ((x = u \land z = v) \to ψ) \leftrightarrow \forall z \forall x ((x = u \land z = v) \to ψ)$
8		ancomst	$⊢ ((x = u \land z = v) \to ψ) \leftrightarrow ((z = v \land x = u) \to ψ)$
9	8	2albii	$⊢ \forall z \forall x ((x = u \land z = v) \to ψ) \leftrightarrow \forall z \forall x ((z = v \land x = u) \to ψ)$
10	7 9	bitri	$⊢ \forall x \forall z ((x = u \land z = v) \to ψ) \leftrightarrow \forall z \forall x ((z = v \land x = u) \to ψ)$
11	6 10	bitrdi	$⊢ \neg \forall z z = x \to ([u/ x] [v/ z] ψ \leftrightarrow \forall z \forall x ((z = v \land x = u) \to ψ))$
12	11	naecoms	$⊢ \neg \forall x x = z \to ([u/ x] [v/ z] ψ \leftrightarrow \forall z \forall x ((z = v \land x = u) \to ψ))$
13		wl-sbcom2d-lem2	$⊢ \neg \forall x x = z \to ([v/ z] [u/ x] ψ \leftrightarrow \forall z \forall x ((z = v \land x = u) \to ψ))$
14	12 13	bitr4d	$⊢ \neg \forall x x = z \to ([u/ x] [v/ z] ψ \leftrightarrow [v/ z] [u/ x] ψ)$
15	2 14	syl	$⊢ φ \to ([u/ x] [v/ z] ψ \leftrightarrow [v/ z] [u/ x] ψ)$
16	15	adantl	$⊢ ((u = y \land v = w) \land φ) \to ([u/ x] [v/ z] ψ \leftrightarrow [v/ z] [u/ x] ψ)$
17		wl-sbcom2d-lem1	$⊢ (u = y \land v = w) \to (\neg \forall x x = w \to ([u/ x] [v/ z] ψ \leftrightarrow [y/ x] [w/ z] ψ))$
18	1 17	syl5	$⊢ (u = y \land v = w) \to (φ \to ([u/ x] [v/ z] ψ \leftrightarrow [y/ x] [w/ z] ψ))$
19	18	imp	$⊢ ((u = y \land v = w) \land φ) \to ([u/ x] [v/ z] ψ \leftrightarrow [y/ x] [w/ z] ψ)$
20		wl-sbcom2d-lem1	$⊢ (v = w \land u = y) \to (\neg \forall z z = y \to ([v/ z] [u/ x] ψ \leftrightarrow [w/ z] [y/ x] ψ))$
21	3 20	syl5	$⊢ (v = w \land u = y) \to (φ \to ([v/ z] [u/ x] ψ \leftrightarrow [w/ z] [y/ x] ψ))$
22	21	ancoms	$⊢ (u = y \land v = w) \to (φ \to ([v/ z] [u/ x] ψ \leftrightarrow [w/ z] [y/ x] ψ))$
23	22	imp	$⊢ ((u = y \land v = w) \land φ) \to ([v/ z] [u/ x] ψ \leftrightarrow [w/ z] [y/ x] ψ)$
24	16 19 23	3bitr3rd	$⊢ ((u = y \land v = w) \land φ) \to ([w/ z] [y/ x] ψ \leftrightarrow [y/ x] [w/ z] ψ)$
25	24	exp31	$⊢ u = y \to (v = w \to (φ \to ([w/ z] [y/ x] ψ \leftrightarrow [y/ x] [w/ z] ψ)))$
26	25	exlimdv	$⊢ u = y \to (\exists v v = w \to (φ \to ([w/ z] [y/ x] ψ \leftrightarrow [y/ x] [w/ z] ψ)))$
27	26	exlimiv	$⊢ \exists u u = y \to (\exists v v = w \to (φ \to ([w/ z] [y/ x] ψ \leftrightarrow [y/ x] [w/ z] ψ)))$
28	4 5 27	mp2	$⊢ φ \to ([w/ z] [y/ x] ψ \leftrightarrow [y/ x] [w/ z] ψ)$

Metamath Proof Explorer

Theorem wl-sbcom2d

Proof