Definition df-ss 3183

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3217). For a more traditional definition, but requiring a dummy variable, see ssalel 3185. Other possible definitions are given by dfss3 3186, ssequn1 3347, ssequn2 3350, and sseqin2 3396. (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 3170	. 2 wff A C_ B
4	1, 2	cin 3169	. . 3 class ( A i^i B )
5	4, 1	wceq 1373	. 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  3184  dfss2  3187  dfss1  3381  inabs  3409  dfrab3ss  3455  disjssun  3528  riinm  4006  rintm  4026  ssex  4189  op1stb  4533  op1stbg  4534  ssdmres  4990  resima2  5002  xpssres  5003  fnimaeq0  5407  f0rn0  5482  fnreseql  5703  tpostpos2  6364  tfrexlem  6433  ecinxp  6710  uzin  9701  iooval2  10057  minmax  11616  xrminmax  11651  2prm  12524  dfphi2  12617  ressbas2d  12975  ressval3d  12979  restid2  13155  lidlbas  14315  difopn  14655  restopnb  14728  cnrest2  14783  bdssex  15976