ax13lem2

Description: Lemma for nfeqf2 . This lemma is equivalent to ax13v with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax13lem2	$⊢ \neg x = y \to (\exists x z = y \to z = y)$

Proof

Step	Hyp	Ref	Expression
1		ax13lem1	$⊢ \neg x = y \to (w = y \to \forall x w = y)$
2		equeucl	$⊢ z = y \to (w = y \to z = w)$
3	2	eximi	$⊢ \exists x z = y \to \exists x (w = y \to z = w)$
4		19.36v	$⊢ \exists x (w = y \to z = w) \leftrightarrow (\forall x w = y \to z = w)$
5	3 4	sylib	$⊢ \exists x z = y \to (\forall x w = y \to z = w)$
6	1 5	syl9	$⊢ \neg x = y \to (\exists x z = y \to (w = y \to z = w))$
7	6	alrimdv	$⊢ \neg x = y \to (\exists x z = y \to \forall w (w = y \to z = w))$
8		equequ2	$⊢ w = y \to (z = w \leftrightarrow z = y)$
9	8	equsalvw	$⊢ \forall w (w = y \to z = w) \leftrightarrow z = y$
10	7 9	imbitrdi	$⊢ \neg x = y \to (\exists x z = y \to z = y)$

Metamath Proof Explorer

Theorem ax13lem2

Proof