Definition df-ss 3128

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3161). For a more traditional definition, but requiring a dummy variable, see dfss2 3130. Other possible definitions are given by dfss3 3131, ssequn1 3291, ssequn2 3294, and sseqin2 3340. (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 3115	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3114	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1343	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 104	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3129  dfss1  3325  inabs  3353  dfrab3ss  3399  disjssun  3471  riinm  3937  rintm  3957  ssex  4118  op1stb  4455  op1stbg  4456  ssdmres  4905  resima2  4917  xpssres  4918  fnimaeq0  5308  f0rn0  5381  fnreseql  5594  tpostpos2  6229  tfrexlem  6298  ecinxp  6572  uzin  9494  iooval2  9847  minmax  11167  xrminmax  11202  2prm  12055  dfphi2  12148  restid2  12560  difopn  12708  restopnb  12781  cnrest2  12836  bdssex  13744