Definition df-ss 3210

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3244). For a more traditional definition, but requiring a dummy variable, see ssalel 3212. Other possible definitions are given by dfss3 3213, ssequn1 3374, ssequn2 3377, and sseqin2 3423. (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 3197	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3196	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1395	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3211  dfss2  3214  dfss1  3408  inabs  3436  dfrab3ss  3482  disjssun  3555  riinm  4038  rintm  4058  ssex  4221  op1stb  4569  op1stbg  4570  ssdmres  5027  resima2  5039  xpssres  5040  fnimaeq0  5445  f0rn0  5522  fnreseql  5747  tpostpos2  6417  tfrexlem  6486  ecinxp  6765  uzin  9763  iooval2  10119  minmax  11749  xrminmax  11784  2prm  12657  dfphi2  12750  ressbas2d  13109  ressval3d  13113  restid2  13289  lidlbas  14450  difopn  14790  restopnb  14863  cnrest2  14918  bdssex  16289