Definition df-ss 2931

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 2964). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 2933). For a more traditional definition, but requiring a dummy variable, see dfss2 2934 (or dfss3 2935 which is similar). (Contributed by NM, 27-Apr-1994.)

Assertion

Ref	Expression
df-ss	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Detailed syntax breakdown of Definition df-ss

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wss 2917	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 2916	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1243	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 98	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  2932  dfss1  3141  inabs  3168  nssinpss  3169  dfrab3ss  3215  disjssun  3285  riinm  3729  rintm  3744  ssex  3894  op1stb  4209  op1stbg  4210  ssdmres  4633  resima2  4644  xpssres  4645  fnimaeq0  5020  fnreseql  5277  tpostpos2  5880  tfrexlem  5948  ecinxp  6181  uzin  8505  iooval2  8784  bdssex  10022