fun0 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem fun0 3530

Description: The empty set is a function. Theorem 10.3 of [Quine] p. 65.

**Assertion**
Ref	Expression
fun0

**Proof of Theorem fun0**
Step	Hyp	Ref	Expression
1		0ss 2291	. 2
2		0ex 2701	. . 3
3	2, 2	funsn 3529	. 2
4		funss 3520	. 2
5	1, 3, 4	mp2 43	1

Colors of variables: wff set class

Syntax hints:

wss 2037

c0 2270

csn 2399

cop 2401

wfun 3166

This theorem is referenced by: fn0 3591 f10 3698 0alg 10533

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-11 964 ax-12 965 ax-13 966 ax-14 967 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 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-pw 2392 df-sn 2402 df-pr 2403 df-op 2406 df-br 2610 df-opab 2657 df-id 2824 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-fun 3182