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 = (/) -> -. A = { (/) } )

Proof

Step Hyp Ref Expression
1 0nep0 
 |-  (/) =/= { (/) }
2 neeq1 
 |-  ( A = (/) -> ( A =/= { (/) } <-> (/) =/= { (/) } ) )
3 1 2 mpbiri 
 |-  ( A = (/) -> A =/= { (/) } )
4 3 neneqd 
 |-  ( A = (/) -> -. A = { (/) } )