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  6541  tfrexlem  6610  ecinxp  6889  uzin  9970  iooval2  10333  minmax  12019  xrminmax  12055  2prm  12929  dfphi2  13026  ressbas2d  13480  ressval3d  13484  restid2  13660  gsummptfidmsplit  14253  gsumresfi  14262  lidlbas  14923  difopn  15351  restopnb  15424  cnrest2  15479  bdssex  17150