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