Definition df-ss 3233

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3268). For a more traditional definition, but requiring a dummy variable, see ssalel 3235. Other possible definitions are given by dfss3 3236, ssequn1 3399, ssequn2 3402, and sseqin2 3450. (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 3220	. 2 wff A C_ B
4	1, 2	cin 3219	. . 3 class ( A i^i B )
5	4, 1	wceq 1402	. 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  3234  dfss2  3237  dfss1  3435  inabs  3463  dfrab3ss  3511  disjssun  3588  riinm  4083  rintm  4103  ssex  4268  op1stb  4622  op1stbg  4623  ssdmres  5083  resima2  5095  xpssres  5096  fnimaeq0  5503  f0rn0  5585  fnreseql  5813  tpostpos2  6529  tfrexlem  6598  ecinxp  6877  uzin  9937  iooval2  10299  minmax  11977  xrminmax  12012  2prm  12886  dfphi2  12979  ressbas2d  13402  ressval3d  13406  restid2  13582  lidlbas  14790  difopn  15135  restopnb  15208  cnrest2  15263  bdssex  16845