Definition df-ss 3170

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3204). For a more traditional definition, but requiring a dummy variable, see ssalel 3172. Other possible definitions are given by dfss3 3173, ssequn1 3334, ssequn2 3337, and sseqin2 3383. (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 3157	. 2 wff A C_ B
4	1, 2	cin 3156	. . 3 class ( A i^i B )
5	4, 1	wceq 1364	. 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  3171  dfss2  3174  dfss1  3368  inabs  3396  dfrab3ss  3442  disjssun  3515  riinm  3990  rintm  4010  ssex  4171  op1stb  4514  op1stbg  4515  ssdmres  4969  resima2  4981  xpssres  4982  fnimaeq0  5382  f0rn0  5455  fnreseql  5675  tpostpos2  6332  tfrexlem  6401  ecinxp  6678  uzin  9651  iooval2  10007  minmax  11412  xrminmax  11447  2prm  12320  dfphi2  12413  ressbas2d  12771  ressval3d  12775  restid2  12950  lidlbas  14110  difopn  14428  restopnb  14501  cnrest2  14556  bdssex  15632