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  4524  op1stbg  4525  ssdmres  4980  resima2  4992  xpssres  4993  fnimaeq0  5396  f0rn0  5469  fnreseql  5689  tpostpos2  6350  tfrexlem  6419  ecinxp  6696  uzin  9680  iooval2  10036  minmax  11483  xrminmax  11518  2prm  12391  dfphi2  12484  ressbas2d  12842  ressval3d  12846  restid2  13022  lidlbas  14182  difopn  14522  restopnb  14595  cnrest2  14650  bdssex  15771