wl-sbcom2d-lem1

Description: Lemma used to prove wl-sbcom2d . (Contributed by Wolf Lammen, 10-Aug-2019) (New usage is discouraged.)

		Ref	Expression
	Assertion	wl-sbcom2d-lem1	$⊢ (u = y \land v = w) \to (\neg \forall x x = w \to ([u/ x] [v/ z] φ \leftrightarrow [y/ x] [w/ z] φ))$

Step	Hyp	Ref	Expression
1		nfna1	$⊢ Ⅎ x \neg \forall x x = w$
2		nfeqf2	$⊢ \neg \forall x x = w \to Ⅎ x v = w$
3	1 2	nfan1	$⊢ Ⅎ x (\neg \forall x x = w \land v = w)$
4		sbequ	$⊢ v = w \to ([v/ z] φ \leftrightarrow [w/ z] φ)$
5	4	adantl	$⊢ (\neg \forall x x = w \land v = w) \to ([v/ z] φ \leftrightarrow [w/ z] φ)$
6	3 5	sbbid	$⊢ (\neg \forall x x = w \land v = w) \to ([u/ x] [v/ z] φ \leftrightarrow [u/ x] [w/ z] φ)$
7	6	ancoms	$⊢ (v = w \land \neg \forall x x = w) \to ([u/ x] [v/ z] φ \leftrightarrow [u/ x] [w/ z] φ)$
8		sbequ	$⊢ u = y \to ([u/ x] [w/ z] φ \leftrightarrow [y/ x] [w/ z] φ)$
9	7 8	sylan9bbr	$⊢ (u = y \land (v = w \land \neg \forall x x = w)) \to ([u/ x] [v/ z] φ \leftrightarrow [y/ x] [w/ z] φ)$
10	9	expr	$⊢ (u = y \land v = w) \to (\neg \forall x x = w \to ([u/ x] [v/ z] φ \leftrightarrow [y/ x] [w/ z] φ))$

Metamath Proof Explorer