Definition df-ss 3227

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

This definition is referenced by:  dfss  3228  dfss2  3231  dfss1  3429  inabs  3457  dfrab3ss  3503  disjssun  3576  riinm  4069  rintm  4089  ssex  4252  op1stb  4604  op1stbg  4605  ssdmres  5065  resima2  5077  xpssres  5078  fnimaeq0  5485  f0rn0  5567  fnreseql  5793  tpostpos2  6509  tfrexlem  6578  ecinxp  6857  uzin  9905  iooval2  10267  minmax  11940  xrminmax  11975  2prm  12849  dfphi2  12942  ressbas2d  13365  ressval3d  13369  restid2  13545  lidlbas  14752  difopn  15099  restopnb  15172  cnrest2  15227  bdssex  16798