Definition df-ss 3134

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3167). For a more traditional definition, but requiring a dummy variable, see dfss2 3136. Other possible definitions are given by dfss3 3137, ssequn1 3297, ssequn2 3300, and sseqin2 3346. (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 3121	. 2 wff A C_ B
4	1, 2	cin 3120	. . 3 class ( A i^i B )
5	4, 1	wceq 1348	. 2 wff ( A i^i B ) = A
6	3, 5	wb 104	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3135  dfss1  3331  inabs  3359  dfrab3ss  3405  disjssun  3477  riinm  3943  rintm  3963  ssex  4124  op1stb  4461  op1stbg  4462  ssdmres  4911  resima2  4923  xpssres  4924  fnimaeq0  5317  f0rn0  5390  fnreseql  5603  tpostpos2  6241  tfrexlem  6310  ecinxp  6584  uzin  9506  iooval2  9859  minmax  11180  xrminmax  11215  2prm  12068  dfphi2  12161  restid2  12575  difopn  12861  restopnb  12934  cnrest2  12989  bdssex  13897