Definition df-ss 2925

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 2958). Contrast this relationship with the relationship A C. B (as will be defined in df-pss 2927). For a more traditional definition, but requiring a dummy variable, see dfss2 2928 (or dfss3 2929 which is similar). (Contributed by NM, 27-Apr-1994.)

Assertion

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

Detailed syntax breakdown of Definition df-ss

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wss 2911	. 2 wff A C_ B
4	1, 2	cin 2910	. . 3 class (A i^i B)
5	4, 1	wceq 1242	. 2 wff (A i^i B) = A
6	3, 5	wb 98	1 wff (A C_ B <-> (A i^i B) = A)

This definition is referenced by:  dfss  2926  dfss1  3135  inabs  3162  nssinpss  3163  dfrab3ss  3209  disjssun  3279  riinm  3720  rintm  3735  ssex  3885  op1stb  4175  op1stbg  4176  ssdmres  4576  resima2  4587  xpssres  4588  fnimaeq0  4963  fnreseql  5220  tpostpos2  5821  tfrexlem  5889  ecinxp  6117  uzin  8241  iooval2  8514  bdssex  9287