Definition df-ss 3143

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3176). For a more traditional definition, but requiring a dummy variable, see dfss2 3145. Other possible definitions are given by dfss3 3146, ssequn1 3306, ssequn2 3309, and sseqin2 3355. (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 3130	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3129	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1353	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3144  dfss1  3340  inabs  3368  dfrab3ss  3414  disjssun  3487  riinm  3960  rintm  3980  ssex  4141  op1stb  4479  op1stbg  4480  ssdmres  4930  resima2  4942  xpssres  4943  fnimaeq0  5338  f0rn0  5411  fnreseql  5627  tpostpos2  6266  tfrexlem  6335  ecinxp  6610  uzin  9560  iooval2  9915  minmax  11238  xrminmax  11273  2prm  12127  dfphi2  12220  ressbas2d  12528  ressval3d  12531  restid2  12697  difopn  13611  restopnb  13684  cnrest2  13739  bdssex  14657