Definition df-ss 3001

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3033). For a more traditional definition, but requiring a dummy variable, see dfss2 3003. Other possible definitions are given by dfss3 3004, ssequn1 3159, ssequn2 3162, and sseqin2 3208. (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 2988	. 2 wff A C_ B
4	1, 2	cin 2987	. . 3 class ( A i^i B )
5	4, 1	wceq 1287	. 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  3002  dfss1  3193  inabs  3220  dfrab3ss  3266  disjssun  3334  riinm  3787  rintm  3802  ssex  3953  op1stb  4275  op1stbg  4276  ssdmres  4704  resima2  4715  xpssres  4716  fnimaeq0  5102  f0rn0  5170  fnreseql  5374  tpostpos2  5986  tfrexlem  6055  ecinxp  6321  uzin  8986  iooval2  9268  minmax  10559  2prm  11015  dfphi2  11102  bdssex  11262