Theorem aev-o

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 . Version of aev using ax-c11 . (Contributed by NM, 8-Nov-2006) (Proof shortened by Andrew Salmon, 21-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	aev-o	$$⊢\forall xx=y\to \forall zw=v$$

Proof

Step	Hyp	Ref	Expression
1		hbae-o	$$⊢\forall xx=y\to \forall z\forall xx=y$$
2		hbae-o	$$⊢\forall xx=y\to \forall t\forall xx=y$$
3		ax7	$$⊢x=t\to \left(x=y\to t=y\right)$$
4	3	spimvw	$$⊢\forall xx=y\to t=y$$
5	2 4	alrimih	$$⊢\forall xx=y\to \forall tt=y$$
6		ax7	$$⊢y=u\to \left(y=t\to u=t\right)$$
7		equcomi	$$⊢u=t\to t=u$$
8	6 7	syl6	$$⊢y=u\to \left(y=t\to t=u\right)$$
9	8	spimvw	$$⊢\forall yy=t\to t=u$$
10	9	aecoms-o	$$⊢\forall tt=y\to t=u$$
11	10	axc4i-o	$$⊢\forall tt=y\to \forall tt=u$$
12		hbae-o	$$⊢\forall tt=u\to \forall v\forall tt=u$$
13		ax7	$$⊢t=v\to \left(t=u\to v=u\right)$$
14	13	spimvw	$$⊢\forall tt=u\to v=u$$
15	12 14	alrimih	$$⊢\forall tt=u\to \forall vv=u$$
16		aecom-o	$$⊢\forall vv=u\to \forall uu=v$$
17	11 15 16	3syl	$$⊢\forall tt=y\to \forall uu=v$$
18		ax7	$$⊢u=w\to \left(u=v\to w=v\right)$$
19	18	spimvw	$$⊢\forall uu=v\to w=v$$
20	5 17 19	3syl	$$⊢\forall xx=y\to w=v$$
21	1 20	alrimih	$$⊢\forall xx=y\to \forall zw=v$$