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 x y ¬ x = y

Proof

Step Hyp Ref Expression
1 exel x z z x
2 ax-nul y z ¬ z y
3 exdistrv x y z z x z ¬ z y x z z x y z ¬ z y
4 1 2 3 mpbir2an x y z z x z ¬ z y
5 ax9v1 x = y z x z y
6 5 eximdv x = y z z x z z y
7 df-ex z z y ¬ z ¬ z y
8 6 7 imbitrdi x = y z z x ¬ z ¬ z y
9 8 com12 z z x x = y ¬ z ¬ z y
10 9 con2d z z x z ¬ z y ¬ x = y
11 10 imp z z x z ¬ z y ¬ x = y
12 11 2eximi x y z z x z ¬ z y x y ¬ x = y
13 4 12 ax-mp x y ¬ x = y