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

Metamath Proof Explorer

Theorem ax6vsep

Description: Derive ax6v (a weakened version of ax-6 where x and y must be distinct), from Separation ax-sep and Extensionality ax-ext . See ax6 for the derivation of ax-6 from ax6v . (Contributed by NM, 12-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6vsep 
|- -. A. x -. x = y

Proof

Step Hyp Ref Expression
1 ax-sep 
 |-  E. x A. z ( z e. x <-> ( z e. y /\ ( z = z -> z = z ) ) )
2 id 
 |-  ( z = z -> z = z )
3 2 biantru 
 |-  ( z e. y <-> ( z e. y /\ ( z = z -> z = z ) ) )
4 3 bibi2i 
 |-  ( ( z e. x <-> z e. y ) <-> ( z e. x <-> ( z e. y /\ ( z = z -> z = z ) ) ) )
5 4 biimpri 
 |-  ( ( z e. x <-> ( z e. y /\ ( z = z -> z = z ) ) ) -> ( z e. x <-> z e. y ) )
6 5 alimi 
 |-  ( A. z ( z e. x <-> ( z e. y /\ ( z = z -> z = z ) ) ) -> A. z ( z e. x <-> z e. y ) )
7 ax-ext 
 |-  ( A. z ( z e. x <-> z e. y ) -> x = y )
8 6 7 syl 
 |-  ( A. z ( z e. x <-> ( z e. y /\ ( z = z -> z = z ) ) ) -> x = y )
9 8 eximi 
 |-  ( E. x A. z ( z e. x <-> ( z e. y /\ ( z = z -> z = z ) ) ) -> E. x x = y )
10 1 9 ax-mp 
 |-  E. x x = y
11 df-ex 
 |-  ( E. x x = y <-> -. A. x -. x = y )
12 10 11 mpbi 
 |-  -. A. x -. x = y