Definition df-ss 3233

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3268). For a more traditional definition, but requiring a dummy variable, see ssalel 3235. Other possible definitions are given by dfss3 3236, ssequn1 3399, ssequn2 3402, and sseqin2 3450. (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 3220	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3219	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1402	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is used by:  dfss  3234  dfss2  3237  dfss1  3435  inabs  3463  dfrab3ss  3511  disjssun  3588  riinm  4085  rintm  4105  ssex  4272  op1stb  4626  op1stbg  4627  ssdmres  5087  resima2  5099  xpssres  5100  fnimaeq0  5508  f0rn0  5590  fnreseql  5822  tpostpos2  6540  tfrexlem  6609  ecinxp  6888  uzin  9971  iooval2  10334  minmax  12020  xrminmax  12056  2prm  12930  dfphi2  13027  ressbas2d  13481  ressval3d  13485  restid2  13661  gsummptfidmsplit  14254  gsumresfi  14263  lidlbas  14924  difopn  15334  restopnb  15407  cnrest2  15462  bdssex  17133