Metamath Proof Explorer

Theorem pssn0

Description: A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Assertion pssn0 
|- ( A C. B -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 npss0 
 |-  -. A C. (/)
2 psseq2 
 |-  ( B = (/) -> ( A C. B <-> A C. (/) ) )
3 1 2 mtbiri 
 |-  ( B = (/) -> -. A C. B )
4 3 necon2ai 
 |-  ( A C. B -> B =/= (/) )