Definition df-ss 2997

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3029). For a more traditional definition, but requiring a dummy variable, see dfss2 2999. Other possible definitions are given by dfss3 3000, ssequn1 3154, ssequn2 3157, and sseqin2 3203. (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 2984	. 2 wff A C_ B
4	1, 2	cin 2983	. . 3 class ( A i^i B )
5	4, 1	wceq 1285	. 2 wff ( A i^i B ) = A
6	3, 5	wb 103	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  2998  dfss1  3188  inabs  3215  dfrab3ss  3260  disjssun  3328  riinm  3776  rintm  3791  ssex  3941  op1stb  4262  op1stbg  4263  ssdmres  4691  resima2  4702  xpssres  4703  fnimaeq0  5087  f0rn0  5152  fnreseql  5353  tpostpos2  5961  tfrexlem  6030  ecinxp  6296  uzin  8945  iooval2  9227  minmax  10485  2prm  10888  dfphi2  10975  bdssex  11135