# 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