Definition df-ss 1492

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 1497. Other possible definitions are given by dfss3 1498, dfss4 1667, sspss 1569, ssequn1 1628, ssequn2 1631, sseqin2 1656, and ssdif0 1748.

Assertion

Ref	Expression
df-ss	⊢ (A ⊆ B ↔ (A ∩ 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 1487	. 2 wff A ⊆ B
4	1, 2	cin 1486	. . 3 class (A ∩ B)
5	4, 1	wceq 1091	. 2 wff (A ∩ B) = A
6	3, 5	wb 127	1 wff (A ⊆ B ↔ (A ∩ B) = A)

This definition is referenced by:  dfss 1493  sseqin2 1656  ssin 1659  ssex 1700  op1stb 1992  ordtri3or 2230  ssdmres 2585

metamath.org