This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. See dtruALT and dtruALT2 for alternate proofs avoiding ax-pr . (Contributed by NM, 7-Nov-2006) Extract exneq as an intermediate result. (Revised by BJ, 2-Jan-2025)

		Ref	Expression
	Assertion	dtru	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		exneq	⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦
2		exnal	⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
3	1 2	mpbi	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦