Theorem wl-aleq

Description: The semantics of A. x y = z . (Contributed by Wolf Lammen, 27-Apr-2018)

	Ref	Expression
Assertion	wl-aleq	|- ( A. x y = z <-> ( y = z /\ ( A. x x = y <-> A. x x = z ) ) )

Proof

Step	Hyp	Ref	Expression
1		sp	|- ( A. x y = z -> y = z )
2		equequ2	|- ( y = z -> ( x = y <-> x = z ) )
3	2	alimi	|- ( A. x y = z -> A. x ( x = y <-> x = z ) )
4		albi	|- ( A. x ( x = y <-> x = z ) -> ( A. x x = y <-> A. x x = z ) )
5	3 4	syl	|- ( A. x y = z -> ( A. x x = y <-> A. x x = z ) )
6	1 5	jca	|- ( A. x y = z -> ( y = z /\ ( A. x x = y <-> A. x x = z ) ) )
7		ax7	|- ( x = y -> ( x = z -> y = z ) )
8	7	al2imi	|- ( A. x x = y -> ( A. x x = z -> A. x y = z ) )
9	8	a1dd	|- ( A. x x = y -> ( A. x x = z -> ( y = z -> A. x y = z ) ) )
10		axc9	|- ( -. A. x x = y -> ( -. A. x x = z -> ( y = z -> A. x y = z ) ) )
11	9 10	bija	|- ( ( A. x x = y <-> A. x x = z ) -> ( y = z -> A. x y = z ) )
12	11	impcom	|- ( ( y = z /\ ( A. x x = y <-> A. x x = z ) ) -> A. x y = z )
13	6 12	impbii	|- ( A. x y = z <-> ( y = z /\ ( A. x x = y <-> A. x x = z ) ) )