Definition df-ss 3227

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3262). For a more traditional definition, but requiring a dummy variable, see ssalel 3229. Other possible definitions are given by dfss3 3230, ssequn1 3393, ssequn2 3396, and sseqin2 3444. (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 3214	. 2 wff A C_ B
4	1, 2	cin 3213	. . 3 class ( A i^i B )
5	4, 1	wceq 1398	. 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  3228  dfss2  3231  dfss1  3429  inabs  3457  dfrab3ss  3503  disjssun  3577  riinm  4070  rintm  4090  ssex  4253  op1stb  4605  op1stbg  4606  ssdmres  5066  resima2  5078  xpssres  5079  fnimaeq0  5486  f0rn0  5568  fnreseql  5794  tpostpos2  6510  tfrexlem  6579  ecinxp  6858  uzin  9909  iooval2  10271  minmax  11945  xrminmax  11980  2prm  12854  dfphi2  12947  ressbas2d  13370  ressval3d  13374  restid2  13550  lidlbas  14757  difopn  15104  restopnb  15177  cnrest2  15232  bdssex  16813