Theorem dtru 5409

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

Syntax hints:  ¬ wn 3  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803

This theorem is referenced by:  brprcneu  6861  zfcndpow  10589