This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0inp0

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

		Ref	Expression
	Assertion	0inp0	$⊢ A = \emptyset \to \neg A = \{\emptyset\}$

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