Theorem dtru 5399

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 2028. The same comments and revision history concerning axiom usage as in exneq 5398 apply. See dtruALT 5346 and dtruALT2 5328 for alternate proofs avoiding ax-pr 5390. (Contributed by NM, 7-Nov-2006.) Extract exneq 5398 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 5398	. 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦
2		exnal 1827	. 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
3	1, 2	mpbi 230	1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦

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 2008  ax-9 2119  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780

This theorem is referenced by:  brprcneu  6851  zfcndpow  10576