Definition df-ss 3214

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3248). For a more traditional definition, but requiring a dummy variable, see ssalel 3216. Other possible definitions are given by dfss3 3217, ssequn1 3379, ssequn2 3382, and sseqin2 3428. (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 3201	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3200	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1398	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3215  dfss2  3218  dfss1  3413  inabs  3441  dfrab3ss  3487  disjssun  3560  riinm  4048  rintm  4068  ssex  4231  op1stb  4581  op1stbg  4582  ssdmres  5041  resima2  5053  xpssres  5054  fnimaeq0  5461  f0rn0  5540  fnreseql  5766  tpostpos2  6474  tfrexlem  6543  ecinxp  6822  uzin  9850  iooval2  10211  minmax  11870  xrminmax  11905  2prm  12779  dfphi2  12872  ressbas2d  13231  ressval3d  13235  restid2  13411  lidlbas  14574  difopn  14919  restopnb  14992  cnrest2  15047  bdssex  16618