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  9964  iooval2  10327  minmax  12011  xrminmax  12047  2prm  12921  dfphi2  13018  ressbas2d  13471  ressval3d  13475  restid2  13651  lidlbas  14864  difopn  15258  restopnb  15331  cnrest2  15386  bdssex  17026