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

Theorem dtru 5441
Description: Given any set (the "𝑦 " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 2027. The same comments and revision history concerning axiom usage as in exneq 5440 apply. See dtruALT 5388 and dtruALT2 5370 for alternate proofs avoiding ax-pr 5432. (Contributed by NM, 7-Nov-2006.) Extract exneq 5440 as an intermediate result. (Revised by BJ, 2-Jan-2025.)
Assertion
Ref Expression
dtru ¬ ∀𝑥 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem dtru
StepHypRef Expression
1 exneq 5440 . 2 𝑥 ¬ 𝑥 = 𝑦
2 exnal 1827 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
31, 2mpbi 230 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1538  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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780
This theorem is referenced by:  brprcneu  6896  zfcndpow  10656
  Copyright terms: Public domain W3C validator