Description: There is only one empty set. (Contributed by RP, 1-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eu0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel | |
|
2 | 1 | ax-gen | |
3 | ax-nul | |
|
4 | nulmo | |
|
5 | df-eu | |
|
6 | 3 4 5 | mpbir2an | |
7 | 2 6 | pm3.2i | |