Theorem dtru 5403

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 2047. The same comments and revision history concerning axiom usage as in exneq 5402 apply. See dtruALT 5344 and dtruALT2 5326 for alternate proofs avoiding ax-pr 5389. (Contributed by NM, 7-Nov-2006.) Extract exneq 5402 as an intermediate result. (Revised by BJ, 2-Jan-2025.)

Assertion

Ref	Expression
dtru	⊢ ¬ ∀𝑥 𝑥 = 𝑦

Distinct variable group:   𝑥,𝑦

Proof of Theorem dtru

Step	Hyp	Ref	Expression
1		exneq 5402	. 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦
2		exnal 1846	. 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
3	1, 2	mpbi 232	1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799

This theorem is referenced by:  brprcneu  6853  zfcndpow  10571