Definition df-ss 2987

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3019). For a more traditional definition, but requiring a dummy variable, see dfss2 2989. Other possible definitions are given by dfss3 2990, ssequn1 3143, ssequn2 3146, and sseqin2 3192. (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 2974	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 2973	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1285	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 103	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  2988  dfss1  3177  inabs  3204  dfrab3ss  3249  disjssun  3314  riinm  3758  rintm  3773  ssex  3923  op1stb  4235  op1stbg  4236  ssdmres  4661  resima2  4672  xpssres  4673  fnimaeq0  5051  fnreseql  5309  tpostpos2  5914  tfrexlem  5983  ecinxp  6247  uzin  8732  iooval2  9014  minmax  10250  2prm  10653  bdssex  10851