Definition df-ss 3142

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

This definition is referenced by:  dfss  3143  dfss1  3339  inabs  3367  dfrab3ss  3413  disjssun  3486  riinm  3959  rintm  3979  ssex  4140  op1stb  4478  op1stbg  4479  ssdmres  4929  resima2  4941  xpssres  4942  fnimaeq0  5337  f0rn0  5410  fnreseql  5626  tpostpos2  6265  tfrexlem  6334  ecinxp  6609  uzin  9559  iooval2  9914  minmax  11237  xrminmax  11272  2prm  12126  dfphi2  12219  ressbas2d  12527  ressval3d  12530  restid2  12696  difopn  13578  restopnb  13651  cnrest2  13706  bdssex  14624