Theorem dtru

Description: Given any set (the " y " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 . The same comments and revision history concerning axiom usage as in exneq apply. (Contributed by NM, 7-Nov-2006) Extract exneq as an intermediate result. (Revised by BJ, 2-Jan-2025)

	Ref	Expression
Assertion	dtru	$$⊢\neg \forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		exneq	$$⊢\exists x\neg x=y$$
2		exnal	$$⊢\exists x\neg x=y\leftrightarrow \neg \forall xx=y$$
3	1 2	mpbi	$$⊢\neg \forall xx=y$$