Theorem hbae-o

Description: All variables are effectively bound in an identical variable specifier. Version of hbae using ax-c11 . (Contributed by NM, 13-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hbae-o	$$⊢\forall xx=y\to \forall z\forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		ax-c5	$$⊢\forall xx=y\to x=y$$
2		ax-c9	$$⊢\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		ax-c11	$$⊢\forall xx=z\to \left(\forall xx=y\to \forall zx=y\right)$$
5	4	aecoms-o	$$⊢\forall zz=x\to \left(\forall xx=y\to \forall zx=y\right)$$
6		ax-c11	$$⊢\forall xx=y\to \left(\forall xx=y\to \forall yx=y\right)$$
7	6	pm2.43i	$$⊢\forall xx=y\to \forall yx=y$$
8		ax-c11	$$⊢\forall yy=z\to \left(\forall yx=y\to \forall zx=y\right)$$
9	7 8	syl5	$$⊢\forall yy=z\to \left(\forall xx=y\to \forall zx=y\right)$$
10	9	aecoms-o	$$⊢\forall zz=y\to \left(\forall xx=y\to \forall zx=y\right)$$
11	3 5 10	pm2.61ii	$$⊢\forall xx=y\to \forall zx=y$$
12	11	axc4i-o	$$⊢\forall xx=y\to \forall x\forall zx=y$$
13		ax-11	$$⊢\forall x\forall zx=y\to \forall z\forall xx=y$$
14	12 13	syl	$$⊢\forall xx=y\to \forall z\forall xx=y$$