Metamath Proof Explorer

Theorem pssirr

Description: Proper subclass is irreflexive. Theorem 7 of Suppes p. 23. (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion pssirr 
|- -. A C. A

Proof

Step Hyp Ref Expression
1 pm3.24 
 |-  -. ( A C_ A /\ -. A C_ A )
2 dfpss3 
 |-  ( A C. A <-> ( A C_ A /\ -. A C_ A ) )
3 1 2 mtbir 
 |-  -. A C. A