MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exexneq Structured version   Visualization version   GIF version

Theorem exexneq 5433
Description: There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2369. (Revised by BJ, 31-May-2019.) Avoid ax-8 2106. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2169. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5426 instead of ax-pow 5362. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5435. (Revised by BJ, 2-Jan-2025.)
Assertion
Ref Expression
exexneq 𝑥𝑦 ¬ 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem exexneq
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 exel 5432 . . 3 𝑥𝑧 𝑧𝑥
2 ax-nul 5305 . . 3 𝑦𝑧 ¬ 𝑧𝑦
3 exdistrv 1957 . . 3 (∃𝑥𝑦(∃𝑧 𝑧𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) ↔ (∃𝑥𝑧 𝑧𝑥 ∧ ∃𝑦𝑧 ¬ 𝑧𝑦))
41, 2, 3mpbir2an 707 . 2 𝑥𝑦(∃𝑧 𝑧𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦)
5 ax9v1 2116 . . . . . . . 8 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
65eximdv 1918 . . . . . . 7 (𝑥 = 𝑦 → (∃𝑧 𝑧𝑥 → ∃𝑧 𝑧𝑦))
7 df-ex 1780 . . . . . . 7 (∃𝑧 𝑧𝑦 ↔ ¬ ∀𝑧 ¬ 𝑧𝑦)
86, 7imbitrdi 250 . . . . . 6 (𝑥 = 𝑦 → (∃𝑧 𝑧𝑥 → ¬ ∀𝑧 ¬ 𝑧𝑦))
98com12 32 . . . . 5 (∃𝑧 𝑧𝑥 → (𝑥 = 𝑦 → ¬ ∀𝑧 ¬ 𝑧𝑦))
109con2d 134 . . . 4 (∃𝑧 𝑧𝑥 → (∀𝑧 ¬ 𝑧𝑦 → ¬ 𝑥 = 𝑦))
1110imp 405 . . 3 ((∃𝑧 𝑧𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) → ¬ 𝑥 = 𝑦)
12112eximi 1836 . 2 (∃𝑥𝑦(∃𝑧 𝑧𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) → ∃𝑥𝑦 ¬ 𝑥 = 𝑦)
134, 12ax-mp 5 1 𝑥𝑦 ¬ 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394  wal 1537  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-9 2114  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780
This theorem is referenced by:  exneq  5434
  Copyright terms: Public domain W3C validator