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  9965  iooval2  10328  minmax  12014  xrminmax  12050  2prm  12924  dfphi2  13021  ressbas2d  13475  ressval3d  13479  restid2  13655  lidlbas  14899  difopn  15300  restopnb  15373  cnrest2  15428  bdssex  17094