Theorem dtru 5446

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 5445 apply. See dtruALT 5393 and dtruALT2 5375 for alternate proofs avoiding ax-pr 5437. (Contributed by NM, 7-Nov-2006.) Extract exneq 5445 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 5445	. 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦
2		exnal 1823	. 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
3	1, 2	mpbi 230	1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1534  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-nul 5311  ax-pr 5437

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

This theorem is referenced by:  brprcneu  6896  zfcndpow  10653