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

Metamath Proof Explorer

Theorem exexneq

Description: There exist two different sets. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by BJ, 31-May-2019) Avoid ax-8 . (Revised by SN, 21-Sep-2023) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) Use ax-pr instead of ax-pow . (Revised by BTernaryTau, 3-Dec-2024) Extract this result from the proof of dtru . (Revised by BJ, 2-Jan-2025)

Ref Expression
Assertion exexneq 
|- E. x E. y -. x = y

Proof

Step Hyp Ref Expression
1 exel 
 |-  E. x E. z z e. x
2 ax-nul 
 |-  E. y A. z -. z e. y
3 exdistrv 
 |-  ( E. x E. y ( E. z z e. x /\ A. z -. z e. y ) <-> ( E. x E. z z e. x /\ E. y A. z -. z e. y ) )
4 1 2 3 mpbir2an 
 |-  E. x E. y ( E. z z e. x /\ A. z -. z e. y )
5 ax9v1 
 |-  ( x = y -> ( z e. x -> z e. y ) )
6 5 eximdv 
 |-  ( x = y -> ( E. z z e. x -> E. z z e. y ) )
7 df-ex 
 |-  ( E. z z e. y <-> -. A. z -. z e. y )
8 6 7 imbitrdi 
 |-  ( x = y -> ( E. z z e. x -> -. A. z -. z e. y ) )
9 8 com12 
 |-  ( E. z z e. x -> ( x = y -> -. A. z -. z e. y ) )
10 9 con2d 
 |-  ( E. z z e. x -> ( A. z -. z e. y -> -. x = y ) )
11 10 imp 
 |-  ( ( E. z z e. x /\ A. z -. z e. y ) -> -. x = y )
12 11 2eximi 
 |-  ( E. x E. y ( E. z z e. x /\ A. z -. z e. y ) -> E. x E. y -. x = y )
13 4 12 ax-mp 
 |-  E. x E. y -. x = y