Definition df-ss 3180

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

This definition is referenced by:  dfss  3181  dfss2  3184  dfss1  3378  inabs  3406  dfrab3ss  3452  disjssun  3525  riinm  4002  rintm  4022  ssex  4185  op1stb  4529  op1stbg  4530  ssdmres  4986  resima2  4998  xpssres  4999  fnimaeq0  5403  f0rn0  5477  fnreseql  5697  tpostpos2  6358  tfrexlem  6427  ecinxp  6704  uzin  9688  iooval2  10044  minmax  11585  xrminmax  11620  2prm  12493  dfphi2  12586  ressbas2d  12944  ressval3d  12948  restid2  13124  lidlbas  14284  difopn  14624  restopnb  14697  cnrest2  14752  bdssex  15912