Metamath Proof Explorer


Theorem eu0

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

Ref Expression
Assertion eu0 x ¬ x ∃! x y ¬ y x

Proof

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