| 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 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.) |
| Ref | Expression |
|---|---|
| dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exneq 5440 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 | |
| 2 | exnal 1827 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
| 3 | 1, 2 | mpbi 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 |