![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dtru | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exneq 5431 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 | |
2 | exnal 1822 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
3 | 1, 2 | mpbi 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 |