Definition df-ss 3144

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3177). For a more traditional definition, but requiring a dummy variable, see dfss2 3146. Other possible definitions are given by dfss3 3147, ssequn1 3307, ssequn2 3310, and sseqin2 3356. (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 3131	. 2 wff A C_ B
4	1, 2	cin 3130	. . 3 class ( A i^i B )
5	4, 1	wceq 1353	. 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  3145  dfss1  3341  inabs  3369  dfrab3ss  3415  disjssun  3488  riinm  3961  rintm  3981  ssex  4142  op1stb  4480  op1stbg  4481  ssdmres  4931  resima2  4943  xpssres  4944  fnimaeq0  5339  f0rn0  5412  fnreseql  5628  tpostpos2  6268  tfrexlem  6337  ecinxp  6612  uzin  9562  iooval2  9917  minmax  11240  xrminmax  11275  2prm  12129  dfphi2  12222  ressbas2d  12530  ressval3d  12533  restid2  12702  difopn  13693  restopnb  13766  cnrest2  13821  bdssex  14739