Definition df-ss 3210

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3244). For a more traditional definition, but requiring a dummy variable, see ssalel 3212. Other possible definitions are given by dfss3 3213, ssequn1 3374, ssequn2 3377, and sseqin2 3423. (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 3197	. 2 wff A C_ B
4	1, 2	cin 3196	. . 3 class ( A i^i B )
5	4, 1	wceq 1395	. 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  3211  dfss2  3214  dfss1  3408  inabs  3436  dfrab3ss  3482  disjssun  3555  riinm  4038  rintm  4058  ssex  4221  op1stb  4569  op1stbg  4570  ssdmres  5027  resima2  5039  xpssres  5040  fnimaeq0  5445  f0rn0  5522  fnreseql  5747  tpostpos2  6417  tfrexlem  6486  ecinxp  6765  uzin  9767  iooval2  10123  minmax  11756  xrminmax  11791  2prm  12664  dfphi2  12757  ressbas2d  13116  ressval3d  13120  restid2  13296  lidlbas  14457  difopn  14797  restopnb  14870  cnrest2  14925  bdssex  16320