0inp0 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 0inp0 2733

Description: Something cannot be equal to both the null set and the power set of the null set.

**Assertion**
Ref	Expression
0inp0

**Proof of Theorem 0inp0**
Step	Hyp	Ref	Expression
1		0nep0 2732	. . 3
2		neeq1 1587	. . 3
3	1, 2	mpbiri 194	. 2
4		df-ne 1584	. 2
5	3, 4	sylib 198	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wceq 954

wne 1582

c0 2276

csn 2405

This theorem is referenced by: dtru 2767 zfpair 2772

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-10 964 ax-11 965 ax-12 966 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-nul 2705

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-v 1808 df-dif 2045 df-un 2046 df-nul 2277 df-sn 2408 df-pr 2409