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

Theorem dtru 5432
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 2024. The same comments and revision history concerning axiom usage as in exneq 5431 apply. (Contributed by NM, 7-Nov-2006.) Extract exneq 5431 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 5431 . 2 𝑥 ¬ 𝑥 = 𝑦
2 exnal 1822 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
31, 2mpbi 229 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1532  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-nul 5300  ax-pr 5423
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775
This theorem is referenced by:  brprcneu  6881  zfcndpow  10633
  Copyright terms: Public domain W3C validator