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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑤 = 𝑣 )

Proof

Step	Hyp	Ref	Expression
1		hbae-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑥 𝑥 = 𝑦 )
2		hbae-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑡 ∀ 𝑥 𝑥 = 𝑦 )
3		ax7	⊢ ( 𝑥 = 𝑡 → ( 𝑥 = 𝑦 → 𝑡 = 𝑦 ) )
4	3	spimvw	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑡 = 𝑦 )
5	2 4	alrimih	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑡 𝑡 = 𝑦 )
6		ax7	⊢ ( 𝑦 = 𝑢 → ( 𝑦 = 𝑡 → 𝑢 = 𝑡 ) )
7		equcomi	⊢ ( 𝑢 = 𝑡 → 𝑡 = 𝑢 )
8	6 7	syl6	⊢ ( 𝑦 = 𝑢 → ( 𝑦 = 𝑡 → 𝑡 = 𝑢 ) )
9	8	spimvw	⊢ ( ∀ 𝑦 𝑦 = 𝑡 → 𝑡 = 𝑢 )
10	9	aecoms-o	⊢ ( ∀ 𝑡 𝑡 = 𝑦 → 𝑡 = 𝑢 )
11	10	axc4i-o	⊢ ( ∀ 𝑡 𝑡 = 𝑦 → ∀ 𝑡 𝑡 = 𝑢 )
12		hbae-o	⊢ ( ∀ 𝑡 𝑡 = 𝑢 → ∀ 𝑣 ∀ 𝑡 𝑡 = 𝑢 )
13		ax7	⊢ ( 𝑡 = 𝑣 → ( 𝑡 = 𝑢 → 𝑣 = 𝑢 ) )
14	13	spimvw	⊢ ( ∀ 𝑡 𝑡 = 𝑢 → 𝑣 = 𝑢 )
15	12 14	alrimih	⊢ ( ∀ 𝑡 𝑡 = 𝑢 → ∀ 𝑣 𝑣 = 𝑢 )
16		aecom-o	⊢ ( ∀ 𝑣 𝑣 = 𝑢 → ∀ 𝑢 𝑢 = 𝑣 )
17	11 15 16	3syl	⊢ ( ∀ 𝑡 𝑡 = 𝑦 → ∀ 𝑢 𝑢 = 𝑣 )
18		ax7	⊢ ( 𝑢 = 𝑤 → ( 𝑢 = 𝑣 → 𝑤 = 𝑣 ) )
19	18	spimvw	⊢ ( ∀ 𝑢 𝑢 = 𝑣 → 𝑤 = 𝑣 )
20	5 17 19	3syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑤 = 𝑣 )
21	1 20	alrimih	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑤 = 𝑣 )