Definition df-ss 3211

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

This definition is referenced by:  dfss  3212  dfss2  3215  dfss1  3409  inabs  3437  dfrab3ss  3483  disjssun  3556  riinm  4039  rintm  4059  ssex  4222  op1stb  4571  op1stbg  4572  ssdmres  5031  resima2  5043  xpssres  5044  fnimaeq0  5449  f0rn0  5526  fnreseql  5751  tpostpos2  6424  tfrexlem  6493  ecinxp  6772  uzin  9777  iooval2  10138  minmax  11778  xrminmax  11813  2prm  12686  dfphi2  12779  ressbas2d  13138  ressval3d  13142  restid2  13318  lidlbas  14479  difopn  14819  restopnb  14892  cnrest2  14947  bdssex  16407