Definition df-ss 3134

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3167). For a more traditional definition, but requiring a dummy variable, see dfss2 3136. Other possible definitions are given by dfss3 3137, ssequn1 3297, ssequn2 3300, and sseqin2 3346. (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 3121	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3120	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1348	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 104	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3135  dfss1  3331  inabs  3359  dfrab3ss  3405  disjssun  3478  riinm  3945  rintm  3965  ssex  4126  op1stb  4463  op1stbg  4464  ssdmres  4913  resima2  4925  xpssres  4926  fnimaeq0  5319  f0rn0  5392  fnreseql  5606  tpostpos2  6244  tfrexlem  6313  ecinxp  6588  uzin  9519  iooval2  9872  minmax  11193  xrminmax  11228  2prm  12081  dfphi2  12174  restid2  12588  difopn  12902  restopnb  12975  cnrest2  13030  bdssex  13937