aev-o

Description: A "distinctor elimination" lemma with no disjoint variable conditions 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 x x = y \to \forall z w = v$

Proof

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

Metamath Proof Explorer

Theorem aev-o

Proof