This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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