Definition df-ss 3026

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3059). For a more traditional definition, but requiring a dummy variable, see dfss2 3028. Other possible definitions are given by dfss3 3029, ssequn1 3185, ssequn2 3188, and sseqin2 3234. (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 3013	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3012	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1296	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 104	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3027  dfss1  3219  inabs  3247  dfrab3ss  3293  disjssun  3365  riinm  3824  rintm  3843  ssex  3997  op1stb  4328  op1stbg  4329  ssdmres  4767  resima2  4779  xpssres  4780  fnimaeq0  5169  f0rn0  5240  fnreseql  5448  tpostpos2  6068  tfrexlem  6137  ecinxp  6407  uzin  9150  iooval2  9481  minmax  10792  xrminmax  10824  2prm  11551  dfphi2  11638  restid2  11828  difopn  11975  restopnb  12048  cnrest2  12102  bdssex  12505