Theorem wl-euequf

Description: euequ proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020)

	Ref	Expression
Assertion	wl-euequf	|- ( -. A. x x = y -> E! x x = y )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	|- E. z z = y
2		nfv	|- F/ z -. A. x x = y
3		nfna1	|- F/ x -. A. x x = y
4		nfeqf2	|- ( -. A. x x = y -> F/ x z = y )
5		equequ2	|- ( y = z -> ( x = y <-> x = z ) )
6	5	equcoms	|- ( z = y -> ( x = y <-> x = z ) )
7	6	a1i	|- ( -. A. x x = y -> ( z = y -> ( x = y <-> x = z ) ) )
8	3 4 7	alrimdd	|- ( -. A. x x = y -> ( z = y -> A. x ( x = y <-> x = z ) ) )
9	2 8	eximd	|- ( -. A. x x = y -> ( E. z z = y -> E. z A. x ( x = y <-> x = z ) ) )
10	1 9	mpi	|- ( -. A. x x = y -> E. z A. x ( x = y <-> x = z ) )
11		eu6	|- ( E! x x = y <-> E. z A. x ( x = y <-> x = z ) )
12	10 11	sylibr	|- ( -. A. x x = y -> E! x x = y )