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