This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( A C. B <-> ( A C_ B /\ A =/= B ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 0 1 wpss 
 |-  A C. B
3 0 1 wss 
 |-  A C_ B
4 0 1 wne 
 |-  A =/= B
5 3 4 wa 
 |-  ( A C_ B /\ A =/= B )
6 2 5 wb 
 |-  ( A C. B <-> ( A C_ B /\ A =/= B ) )