Metamath Proof Explorer


Theorem eu0

Description: There is only one empty set. (Contributed by RP, 1-Oct-2023)

Ref Expression
Assertion eu0 x¬x∃!xy¬yx

Proof

Step Hyp Ref Expression
1 noel ¬x
2 1 ax-gen x¬x
3 ax-nul xy¬yx
4 nulmo *xy¬yx
5 df-eu ∃!xy¬yxxy¬yx*xy¬yx
6 3 4 5 mpbir2an ∃!xy¬yx
7 2 6 pm3.2i x¬x∃!xy¬yx