0nep0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 0nep0		Structured version Visualization version GIF version

Theorem 0nep0 5362

Description: The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)

**Assertion**
Ref	Expression
0nep0	⊢ ∅ ≠ {∅}

**Proof of Theorem 0nep0**
Step	Hyp	Ref	Expression
1		0ex 5311	. . 3 ⊢ ∅ ∈ V
2	1	snnz 4785	. 2 ⊢ {∅} ≠ ∅
3	2	necomi 2992	1 ⊢ ∅ ≠ {∅}

Colors of variables: wff setvar class

Syntax hints: ≠ wne 2937 ∅c0 4326 {csn 4632

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-nul 5310

This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-v 3475 df-dif 3952 df-nul 4327 df-sn 4633

This theorem is referenced by: 0inp0 5363 opthprc 5746 2dom 9061 pw2eng 9109 djuexb 9940 hashge3el3dif 14487 cat1 18093 isusp 24186 bj-1upln0 36521 clsk1indlem0 43502 mnuprdlem1 43740 mnuprdlem2 43741

	
		OSZAR »