Definition df-ss 3190

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3224). For a more traditional definition, but requiring a dummy variable, see ssalel 3192. Other possible definitions are given by dfss3 3193, ssequn1 3354, ssequn2 3357, and sseqin2 3403. (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 3177	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3176	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1375	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3191  dfss2  3194  dfss1  3388  inabs  3416  dfrab3ss  3462  disjssun  3535  riinm  4017  rintm  4037  ssex  4200  op1stb  4546  op1stbg  4547  ssdmres  5003  resima2  5015  xpssres  5016  fnimaeq0  5421  f0rn0  5496  fnreseql  5718  tpostpos2  6381  tfrexlem  6450  ecinxp  6727  uzin  9723  iooval2  10079  minmax  11707  xrminmax  11742  2prm  12615  dfphi2  12708  ressbas2d  13067  ressval3d  13071  restid2  13247  lidlbas  14407  difopn  14747  restopnb  14820  cnrest2  14875  bdssex  16175