Definition df-ss 3154

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3187). For a more traditional definition, but requiring a dummy variable, see dfss2 3156. Other possible definitions are given by dfss3 3157, ssequn1 3317, ssequn2 3320, and sseqin2 3366. (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 3141	. 2 wff A C_ B
4	1, 2	cin 3140	. . 3 class ( A i^i B )
5	4, 1	wceq 1363	. 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  3155  dfss1  3351  inabs  3379  dfrab3ss  3425  disjssun  3498  riinm  3971  rintm  3991  ssex  4152  op1stb  4490  op1stbg  4491  ssdmres  4941  resima2  4953  xpssres  4954  fnimaeq0  5349  f0rn0  5422  fnreseql  5639  tpostpos2  6279  tfrexlem  6348  ecinxp  6623  uzin  9573  iooval2  9928  minmax  11251  xrminmax  11286  2prm  12140  dfphi2  12233  ressbas2d  12541  ressval3d  12545  restid2  12714  lidlbas  13662  difopn  13879  restopnb  13952  cnrest2  14007  bdssex  14925