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 𝑥𝑦 ¬ 𝑥 = 𝑦

Proof

Step Hyp Ref Expression
1 exel 𝑥𝑧 𝑧𝑥
2 ax-nul 𝑦𝑧 ¬ 𝑧𝑦
3 exdistrv ( ∃ 𝑥𝑦 ( ∃ 𝑧 𝑧𝑥 ∧ ∀ 𝑧 ¬ 𝑧𝑦 ) ↔ ( ∃ 𝑥𝑧 𝑧𝑥 ∧ ∃ 𝑦𝑧 ¬ 𝑧𝑦 ) )
4 1 2 3 mpbir2an 𝑥𝑦 ( ∃ 𝑧 𝑧𝑥 ∧ ∀ 𝑧 ¬ 𝑧𝑦 )
5 ax9v1 ( 𝑥 = 𝑦 → ( 𝑧𝑥𝑧𝑦 ) )
6 5 eximdv ( 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧𝑥 → ∃ 𝑧 𝑧𝑦 ) )
7 df-ex ( ∃ 𝑧 𝑧𝑦 ↔ ¬ ∀ 𝑧 ¬ 𝑧𝑦 )
8 6 7 imbitrdi ( 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧𝑥 → ¬ ∀ 𝑧 ¬ 𝑧𝑦 ) )
9 8 com12 ( ∃ 𝑧 𝑧𝑥 → ( 𝑥 = 𝑦 → ¬ ∀ 𝑧 ¬ 𝑧𝑦 ) )
10 9 con2d ( ∃ 𝑧 𝑧𝑥 → ( ∀ 𝑧 ¬ 𝑧𝑦 → ¬ 𝑥 = 𝑦 ) )
11 10 imp ( ( ∃ 𝑧 𝑧𝑥 ∧ ∀ 𝑧 ¬ 𝑧𝑦 ) → ¬ 𝑥 = 𝑦 )
12 11 2eximi ( ∃ 𝑥𝑦 ( ∃ 𝑧 𝑧𝑥 ∧ ∀ 𝑧 ¬ 𝑧𝑦 ) → ∃ 𝑥𝑦 ¬ 𝑥 = 𝑦 )
13 4 12 ax-mp 𝑥𝑦 ¬ 𝑥 = 𝑦