eq0 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem eq0 2284

Description: The empty set has no elements. Theorem 2 of [Suppes] p. 22.

**Assertion**
Ref	Expression
eq0

**Proof of Theorem eq0**
Step	Hyp	Ref	Expression
1		n0 2279	. . 3
2		df-ex 978	. . 3
3	1, 2	bitr 173	. 2
4	3	con4bii 521	1

Colors of variables: wff set class

Syntax hints:

wn 2

wb 146

wal 951

wceq 953

wcel 955

wex 977

c0 2270

This theorem is referenced by: 0el 2286 ssdif0 2317 difin0ss 2322 inssdif0 2323 ralf0 2349 0ex 2701 snex 2740 reldm0 3320 tz6.12-2 3724 uzwo4OLD 6158 uzwo 6387 uzwoOLD 6388

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-v 1803 df-dif 2039 df-nul 2271