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 ¬ 𝐴 ⊊ 𝐴

Proof

Step Hyp Ref Expression
1 pm3.24 ⊢ ¬ ( 𝐴 ⊆ 𝐴 ∧ ¬ 𝐴 ⊆ 𝐴 )
2 dfpss3 ⊢ ( 𝐴 ⊊ 𝐴 ↔ ( 𝐴 ⊆ 𝐴 ∧ ¬ 𝐴 ⊆ 𝐴 ) )
3 1 2 mtbir ⊢ ¬ 𝐴 ⊊ 𝐴