Definition df-ss 3210

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3244). For a more traditional definition, but requiring a dummy variable, see ssalel 3212. Other possible definitions are given by dfss3 3213, ssequn1 3374, ssequn2 3377, and sseqin2 3423. (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 3197	. 2 wff A C_ B
4	1, 2	cin 3196	. . 3 class ( A i^i B )
5	4, 1	wceq 1395	. 2 wff ( A i^i B ) = A
6	3, 5	wb 105	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3211  dfss2  3214  dfss1  3408  inabs  3436  dfrab3ss  3482  disjssun  3555  riinm  4037  rintm  4057  ssex  4220  op1stb  4568  op1stbg  4569  ssdmres  5026  resima2  5038  xpssres  5039  fnimaeq0  5444  f0rn0  5519  fnreseql  5744  tpostpos2  6409  tfrexlem  6478  ecinxp  6755  uzin  9751  iooval2  10107  minmax  11736  xrminmax  11771  2prm  12644  dfphi2  12737  ressbas2d  13096  ressval3d  13100  restid2  13276  lidlbas  14436  difopn  14776  restopnb  14849  cnrest2  14904  bdssex  16223