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  4270  op1stb  4624  op1stbg  4625  ssdmres  5085  resima2  5097  xpssres  5098  fnimaeq0  5505  f0rn0  5587  fnreseql  5819  tpostpos2  6536  tfrexlem  6605  ecinxp  6884  uzin  9955  iooval2  10317  minmax  11996  xrminmax  12031  2prm  12905  dfphi2  12998  ressbas2d  13422  ressval3d  13426  restid2  13602  lidlbas  14815  difopn  15209  restopnb  15282  cnrest2  15337  bdssex  16928