Definition df-ss 3211

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3245). For a more traditional definition, but requiring a dummy variable, see ssalel 3213. Other possible definitions are given by dfss3 3214, ssequn1 3375, ssequn2 3378, and sseqin2 3424. (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 3198	. 2 wff A C_ B
4	1, 2	cin 3197	. . 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  3212  dfss2  3215  dfss1  3409  inabs  3437  dfrab3ss  3483  disjssun  3556  riinm  4041  rintm  4061  ssex  4224  op1stb  4573  op1stbg  4574  ssdmres  5033  resima2  5045  xpssres  5046  fnimaeq0  5451  f0rn0  5528  fnreseql  5753  tpostpos2  6426  tfrexlem  6495  ecinxp  6774  uzin  9779  iooval2  10140  minmax  11781  xrminmax  11816  2prm  12689  dfphi2  12782  ressbas2d  13141  ressval3d  13145  restid2  13321  lidlbas  14482  difopn  14822  restopnb  14895  cnrest2  14950  bdssex  16433