Metamath Proof Explorer


Definition df-pss

Description: Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. For example, { 1 , 2 } C. { 1 , 2 , 3 } ( ex-pss ). Note that -. A C. A (proved in pssirr ). Contrast this relationship with the relationship A C_ B (as defined in df-ss ). Other possible definitions are given by dfpss2 and dfpss3 . (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion df-pss ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴𝐵 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cB 𝐵
2 0 1 wpss 𝐴𝐵
3 0 1 wss 𝐴𝐵
4 0 1 wne 𝐴𝐵
5 3 4 wa ( 𝐴𝐵𝐴𝐵 )
6 2 5 wb ( 𝐴𝐵 ↔ ( 𝐴𝐵𝐴𝐵 ) )