Theorem wl-aleq

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

	Ref	Expression
Assertion	wl-aleq	$$⊢\forall xy=z\leftrightarrow \left(y=z\wedge \left(\forall xx=y\leftrightarrow \forall xx=z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall xy=z\to y=z$$
2		equequ2	$$⊢y=z\to \left(x=y\leftrightarrow x=z\right)$$
3	2	alimi	$$⊢\forall xy=z\to \forall x\left(x=y\leftrightarrow x=z\right)$$
4		albi	$$⊢\forall x\left(x=y\leftrightarrow x=z\right)\to \left(\forall xx=y\leftrightarrow \forall xx=z\right)$$
5	3 4	syl	$$⊢\forall xy=z\to \left(\forall xx=y\leftrightarrow \forall xx=z\right)$$
6	1 5	jca	$$⊢\forall xy=z\to \left(y=z\wedge \left(\forall xx=y\leftrightarrow \forall xx=z\right)\right)$$
7		ax7	$$⊢x=y\to \left(x=z\to y=z\right)$$
8	7	al2imi	$$⊢\forall xx=y\to \left(\forall xx=z\to \forall xy=z\right)$$
9	8	a1dd	$$⊢\forall xx=y\to \left(\forall xx=z\to \left(y=z\to \forall xy=z\right)\right)$$
10		axc9	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=z\to \left(y=z\to \forall xy=z\right)\right)$$
11	9 10	bija	$$⊢\left(\forall xx=y\leftrightarrow \forall xx=z\right)\to \left(y=z\to \forall xy=z\right)$$
12	11	impcom	$$⊢\left(y=z\wedge \left(\forall xx=y\leftrightarrow \forall xx=z\right)\right)\to \forall xy=z$$
13	6 12	impbii	$$⊢\forall xy=z\leftrightarrow \left(y=z\wedge \left(\forall xx=y\leftrightarrow \forall xx=z\right)\right)$$