Definition df-ss 2986

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3018). For a more traditional definition, but requiring a dummy variable, see dfss2 2988. Other possible definitions are given by dfss3 2989, ssequn1 3142, ssequn2 3145, and sseqin2 3185. (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 2973	. 2 wff A C_ B
4	1, 2	cin 2972	. . 3 class ( A i^i B )
5	4, 1	wceq 1284	. 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  2987  dfss1  3170  inabs  3197  dfrab3ss  3242  disjssun  3307  riinm  3750  rintm  3765  ssex  3915  op1stb  4227  op1stbg  4228  ssdmres  4651  resima2  4662  xpssres  4663  fnimaeq0  5040  fnreseql  5298  tpostpos2  5903  tfrexlem  5971  ecinxp  6204  uzin  8651  iooval2  8938  minmax  10112  2prm  10509  bdssex  10693