Definition df-ss 3226

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3260). For a more traditional definition, but requiring a dummy variable, see ssalel 3228. Other possible definitions are given by dfss3 3229, ssequn1 3391, ssequn2 3394, and sseqin2 3442. (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 3213	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3212	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1398	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3227  dfss2  3230  dfss1  3427  inabs  3455  dfrab3ss  3501  disjssun  3574  riinm  4066  rintm  4086  ssex  4249  op1stb  4601  op1stbg  4602  ssdmres  5062  resima2  5074  xpssres  5075  fnimaeq0  5482  f0rn0  5564  fnreseql  5790  tpostpos2  6498  tfrexlem  6567  ecinxp  6846  uzin  9890  iooval2  10251  minmax  11919  xrminmax  11954  2prm  12828  dfphi2  12921  ressbas2d  13298  ressval3d  13302  restid2  13478  lidlbas  14643  difopn  14990  restopnb  15063  cnrest2  15118  bdssex  16689