Definition df-ss 3213

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3247). For a more traditional definition, but requiring a dummy variable, see ssalel 3215. Other possible definitions are given by dfss3 3216, ssequn1 3377, ssequn2 3380, and sseqin2 3426. (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 3200	. 2 wff A C_ B
4	1, 2	cin 3199	. . 3 class ( A i^i B )
5	4, 1	wceq 1397	. 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  3214  dfss2  3217  dfss1  3411  inabs  3439  dfrab3ss  3485  disjssun  3558  riinm  4043  rintm  4063  ssex  4226  op1stb  4575  op1stbg  4576  ssdmres  5035  resima2  5047  xpssres  5048  fnimaeq0  5454  f0rn0  5531  fnreseql  5757  tpostpos2  6431  tfrexlem  6500  ecinxp  6779  uzin  9789  iooval2  10150  minmax  11808  xrminmax  11843  2prm  12717  dfphi2  12810  ressbas2d  13169  ressval3d  13173  restid2  13349  lidlbas  14511  difopn  14851  restopnb  14924  cnrest2  14979  bdssex  16548