Definition df-ss 3213

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3247). For a more traditional definition, but requiring a dummy variable, see ssalel 3215. Other possible definitions are given by dfss3 3216, ssequn1 3377, ssequn2 3380, and sseqin2 3426. (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 3200	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3199	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1397	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3214  dfss2  3217  dfss1  3411  inabs  3439  dfrab3ss  3485  disjssun  3558  riinm  4043  rintm  4063  ssex  4226  op1stb  4575  op1stbg  4576  ssdmres  5035  resima2  5047  xpssres  5048  fnimaeq0  5454  f0rn0  5531  fnreseql  5757  tpostpos2  6431  tfrexlem  6500  ecinxp  6779  uzin  9789  iooval2  10150  minmax  11791  xrminmax  11826  2prm  12700  dfphi2  12793  ressbas2d  13152  ressval3d  13156  restid2  13332  lidlbas  14494  difopn  14834  restopnb  14907  cnrest2  14962  bdssex  16500