Definition df-ss 3166

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3199). For a more traditional definition, but requiring a dummy variable, see dfss2 3168. Other possible definitions are given by dfss3 3169, ssequn1 3329, ssequn2 3332, and sseqin2 3378. (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 3153	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3152	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1364	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3167  dfss1  3363  inabs  3391  dfrab3ss  3437  disjssun  3510  riinm  3985  rintm  4005  ssex  4166  op1stb  4509  op1stbg  4510  ssdmres  4964  resima2  4976  xpssres  4977  fnimaeq0  5375  f0rn0  5448  fnreseql  5668  tpostpos2  6318  tfrexlem  6387  ecinxp  6664  uzin  9625  iooval2  9981  minmax  11373  xrminmax  11408  2prm  12265  dfphi2  12358  ressbas2d  12686  ressval3d  12690  restid2  12859  lidlbas  13974  difopn  14276  restopnb  14349  cnrest2  14404  bdssex  15394