Definition df-ss 3034

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3067). For a more traditional definition, but requiring a dummy variable, see dfss2 3036. Other possible definitions are given by dfss3 3037, ssequn1 3193, ssequn2 3196, and sseqin2 3242. (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 3021	. 2 wff A C_ B
4	1, 2	cin 3020	. . 3 class ( A i^i B )
5	4, 1	wceq 1299	. 2 wff ( A i^i B ) = A
6	3, 5	wb 104	1 wff ( A C_ B <-> ( A i^i B ) = A )

This definition is referenced by:  dfss  3035  dfss1  3227  inabs  3255  dfrab3ss  3301  disjssun  3373  riinm  3832  rintm  3851  ssex  4005  op1stb  4337  op1stbg  4338  ssdmres  4777  resima2  4789  xpssres  4790  fnimaeq0  5180  f0rn0  5253  fnreseql  5462  tpostpos2  6092  tfrexlem  6161  ecinxp  6434  uzin  9208  iooval2  9539  minmax  10840  xrminmax  10873  2prm  11601  dfphi2  11688  restid2  11911  difopn  12059  restopnb  12132  cnrest2  12186  bdssex  12681