Definition df-ss 3178

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3212). For a more traditional definition, but requiring a dummy variable, see ssalel 3180. Other possible definitions are given by dfss3 3181, ssequn1 3342, ssequn2 3345, and sseqin2 3391. (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 3165	. 2 wff A C_ B
4	1, 2	cin 3164	. . 3 class ( A i^i B )
5	4, 1	wceq 1372	. 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  3179  dfss2  3182  dfss1  3376  inabs  3404  dfrab3ss  3450  disjssun  3523  riinm  3999  rintm  4019  ssex  4180  op1stb  4523  op1stbg  4524  ssdmres  4978  resima2  4990  xpssres  4991  fnimaeq0  5391  f0rn0  5464  fnreseql  5684  tpostpos2  6341  tfrexlem  6410  ecinxp  6687  uzin  9663  iooval2  10019  minmax  11460  xrminmax  11495  2prm  12368  dfphi2  12461  ressbas2d  12819  ressval3d  12823  restid2  12998  lidlbas  14158  difopn  14498  restopnb  14571  cnrest2  14626  bdssex  15702