Description: The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996)
Ref | Expression | ||
---|---|---|---|
Assertion | 0pss | |- ( (/) C. A <-> A =/= (/) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss | |- (/) C_ A |
|
2 | df-pss | |- ( (/) C. A <-> ( (/) C_ A /\ (/) =/= A ) ) |
|
3 | 1 2 | mpbiran | |- ( (/) C. A <-> (/) =/= A ) |
4 | necom | |- ( (/) =/= A <-> A =/= (/) ) |
|
5 | 3 4 | bitri | |- ( (/) C. A <-> A =/= (/) ) |