Definition df-ss 3084

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3117). For a more traditional definition, but requiring a dummy variable, see dfss2 3086. Other possible definitions are given by dfss3 3087, ssequn1 3246, ssequn2 3249, and sseqin2 3295. (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 3071	. 2 wff A C_ B
4	1, 2	cin 3070	. . 3 class ( A i^i B )
5	4, 1	wceq 1331	. 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  3085  dfss1  3280  inabs  3308  dfrab3ss  3354  disjssun  3426  riinm  3885  rintm  3905  ssex  4065  op1stb  4399  op1stbg  4400  ssdmres  4841  resima2  4853  xpssres  4854  fnimaeq0  5244  f0rn0  5317  fnreseql  5530  tpostpos2  6162  tfrexlem  6231  ecinxp  6504  uzin  9358  iooval2  9698  minmax  11001  xrminmax  11034  2prm  11808  dfphi2  11896  restid2  12129  difopn  12277  restopnb  12350  cnrest2  12405  bdssex  13100