Theorem 0inp0

Description: Something cannot be equal to both the empty set and the power set of the empty set. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	0inp0	$$⊢A=\varnothing \to \neg A=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
2		neeq1	$$⊢A=\varnothing \to \left(A\ne \left\{\varnothing \right\}\leftrightarrow \varnothing \ne \left\{\varnothing \right\}\right)$$
3	1 2	mpbiri	$$⊢A=\varnothing \to A\ne \left\{\varnothing \right\}$$
4	3	neneqd	$$⊢A=\varnothing \to \neg A=\left\{\varnothing \right\}$$