Theorem 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	|- ( -. x = y -> ( E. x z = y -> z = y ) )

Proof

Step	Hyp	Ref	Expression
1		ax13lem1	|- ( -. x = y -> ( w = y -> A. x w = y ) )
2		equeucl	|- ( z = y -> ( w = y -> z = w ) )
3	2	eximi	|- ( E. x z = y -> E. x ( w = y -> z = w ) )
4		19.36v	|- ( E. x ( w = y -> z = w ) <-> ( A. x w = y -> z = w ) )
5	3 4	sylib	|- ( E. x z = y -> ( A. x w = y -> z = w ) )
6	1 5	syl9	|- ( -. x = y -> ( E. x z = y -> ( w = y -> z = w ) ) )
7	6	alrimdv	|- ( -. x = y -> ( E. x z = y -> A. w ( w = y -> z = w ) ) )
8		equequ2	|- ( w = y -> ( z = w <-> z = y ) )
9	8	equsalvw	|- ( A. w ( w = y -> z = w ) <-> z = y )
10	7 9	syl6ib	|- ( -. x = y -> ( E. x z = y -> z = y ) )