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 
|- ( A. x x = y -> A. z w = v )

Proof

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