Theorem dtru 5404

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812

This theorem is used by:  brprcneu  6875  zfcndpow  10704