Definition df-ss 3170

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3204). For a more traditional definition, but requiring a dummy variable, see ssalel 3172. Other possible definitions are given by dfss3 3173, ssequn1 3334, ssequn2 3337, and sseqin2 3383. (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 3157	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3156	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1364	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3171  dfss2  3174  dfss1  3368  inabs  3396  dfrab3ss  3442  disjssun  3515  riinm  3990  rintm  4010  ssex  4171  op1stb  4514  op1stbg  4515  ssdmres  4969  resima2  4981  xpssres  4982  fnimaeq0  5382  f0rn0  5455  fnreseql  5675  tpostpos2  6332  tfrexlem  6401  ecinxp  6678  uzin  9653  iooval2  10009  minmax  11414  xrminmax  11449  2prm  12322  dfphi2  12415  ressbas2d  12773  ressval3d  12777  restid2  12952  lidlbas  14112  difopn  14430  restopnb  14503  cnrest2  14558  bdssex  15634