Metamath Proof Explorer

Theorem pssirr

Description: Proper subclass is irreflexive. Theorem 7 of Suppes p. 23. (Contributed by NM, 7-Feb-1996) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

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

Proof

Step Hyp Ref Expression
1 neirr 
 |-  -. A =/= A
2 pssne 
 |-  ( A C. A -> A =/= A )
3 1 2 mto 
 |-  -. A C. A