Theorem bj-hbaeb2

Description: Biconditional version of a form of hbae with commuted quantifiers, not requiring ax-11 . (Contributed by BJ, 12-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-hbaeb2	$$⊢\forall xx=y\leftrightarrow \forall x\forall zx=y$$

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall xx=y\to x=y$$
2		axc9	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x=y\to \forall zx=y\right)\right)$$
3	1 2	syl7	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(\forall xx=y\to \forall zx=y\right)\right)$$
4		axc11r	$$⊢\forall zz=x\to \left(\forall xx=y\to \forall zx=y\right)$$
5		axc11	$$⊢\forall xx=y\to \left(\forall xx=y\to \forall yx=y\right)$$
6	5	pm2.43i	$$⊢\forall xx=y\to \forall yx=y$$
7		axc11r	$$⊢\forall zz=y\to \left(\forall yx=y\to \forall zx=y\right)$$
8	6 7	syl5	$$⊢\forall zz=y\to \left(\forall xx=y\to \forall zx=y\right)$$
9	3 4 8	pm2.61ii	$$⊢\forall xx=y\to \forall zx=y$$
10	9	axc4i	$$⊢\forall xx=y\to \forall x\forall zx=y$$
11		sp	$$⊢\forall zx=y\to x=y$$
12	11	alimi	$$⊢\forall x\forall zx=y\to \forall xx=y$$
13	10 12	impbii	$$⊢\forall xx=y\leftrightarrow \forall x\forall zx=y$$