Definition df-ss 3089

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3122). For a more traditional definition, but requiring a dummy variable, see dfss2 3091. Other possible definitions are given by dfss3 3092, ssequn1 3251, ssequn2 3254, and sseqin2 3300. (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 3076	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3075	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1332	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 104	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3090  dfss1  3285  inabs  3313  dfrab3ss  3359  disjssun  3431  riinm  3893  rintm  3913  ssex  4073  op1stb  4407  op1stbg  4408  ssdmres  4849  resima2  4861  xpssres  4862  fnimaeq0  5252  f0rn0  5325  fnreseql  5538  tpostpos2  6170  tfrexlem  6239  ecinxp  6512  uzin  9382  iooval2  9728  minmax  11033  xrminmax  11066  2prm  11844  dfphi2  11932  restid2  12168  difopn  12316  restopnb  12389  cnrest2  12444  bdssex  13271