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. (Contributed by NM, 7-Nov-2006) Extract exneq as an intermediate result. (Revised by BJ, 2-Jan-2025)

Ref Expression
Assertion dtru
|- -. A. x x = y

Proof

Step Hyp Ref Expression
1 exneq
 |-  E. x -. x = y
2 exnal
 |-  ( E. x -. x = y <-> -. A. x x = y )
3 1 2 mpbi
 |-  -. A. x x = y