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

Proof

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