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  6430  tfrexlem  6499  ecinxp  6778  uzin  9788  iooval2  10149  minmax  11790  xrminmax  11825  2prm  12698  dfphi2  12791  ressbas2d  13150  ressval3d  13154  restid2  13330  lidlbas  14491  difopn  14831  restopnb  14904  cnrest2  14959  bdssex  16497