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	⊢ ( 𝐴 = ∅ → ¬ 𝐴 = { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		0nep0	⊢ ∅ ≠ { ∅ }
2		neeq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≠ { ∅ } ↔ ∅ ≠ { ∅ } ) )
3	1 2	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ≠ { ∅ } )
4	3	neneqd	⊢ ( 𝐴 = ∅ → ¬ 𝐴 = { ∅ } )