Definition df-ss

Description: Define the subclass relationship. Exercise 9 of TakeutiZaring p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } ( ex-ss ). Note that A C_ A (proved in ssid ). Contrast this relationship with the relationship A C. B (as will be defined in df-pss ). For a more traditional definition, but requiring a dummy variable, see dfss2 . Other possible definitions are given by dfss3 , dfss4 , sspss , ssequn1 , ssequn2 , sseqin2 , and ssdif0 .

We prefer the label "ss" ("subset") for C_ , despite the fact that it applies to classes. It is much more common to refer to this as the subset relation than subclass, especially since most of the time the arguments are in fact sets (and for pragmatic reasons we don't want to need to use different operations for sets). The way set.mm is set up, many things are technically classes despite morally (and provably) being sets, like 1 (cf. df-1 and 1ex ) or RR ( cf. df-r and reex ). This has to do with the fact that there are no "set expressions": classes are expressions but there are only set variables in set.mm (cf. https://us.metamath.org/downloads/grammar-ambiguity.txt ). This is why we use C_ both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 27-Apr-1994)

	Ref	Expression
Assertion	df-ss	|- ( A C_ B <-> ( A i^i B ) = A )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	wss	|- A C_ B
3	0 1	cin	|- ( A i^i B )
4	3 0	wceq	|- ( A i^i B ) = A
5	2 4	wb	|- ( A C_ B <-> ( A i^i B ) = A )