Definition df-ss 3167

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3200). For a more traditional definition, but requiring a dummy variable, see dfss2 3169. Other possible definitions are given by dfss3 3170, ssequn1 3330, ssequn2 3333, and sseqin2 3379. (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 3154	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3153	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1364	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3168  dfss1  3364  inabs  3392  dfrab3ss  3438  disjssun  3511  riinm  3986  rintm  4006  ssex  4167  op1stb  4510  op1stbg  4511  ssdmres  4965  resima2  4977  xpssres  4978  fnimaeq0  5376  f0rn0  5449  fnreseql  5669  tpostpos2  6320  tfrexlem  6389  ecinxp  6666  uzin  9628  iooval2  9984  minmax  11376  xrminmax  11411  2prm  12268  dfphi2  12361  ressbas2d  12689  ressval3d  12693  restid2  12862  lidlbas  13977  difopn  14287  restopnb  14360  cnrest2  14415  bdssex  15464