Definition df-ss 3144

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3177). For a more traditional definition, but requiring a dummy variable, see dfss2 3146. Other possible definitions are given by dfss3 3147, ssequn1 3307, ssequn2 3310, and sseqin2 3356. (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 3131	. 2 wff 𝐴 ⊆ 𝐵
4	1, 2	cin 3130	. . 3 class (𝐴 ∩ 𝐵)
5	4, 1	wceq 1353	. 2 wff (𝐴 ∩ 𝐵) = 𝐴
6	3, 5	wb 105	1 wff (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

This definition is referenced by:  dfss  3145  dfss1  3341  inabs  3369  dfrab3ss  3415  disjssun  3488  riinm  3961  rintm  3981  ssex  4142  op1stb  4480  op1stbg  4481  ssdmres  4931  resima2  4943  xpssres  4944  fnimaeq0  5339  f0rn0  5412  fnreseql  5629  tpostpos2  6269  tfrexlem  6338  ecinxp  6613  uzin  9563  iooval2  9918  minmax  11241  xrminmax  11276  2prm  12130  dfphi2  12223  ressbas2d  12531  ressval3d  12534  restid2  12703  lidlbas  13601  difopn  13796  restopnb  13869  cnrest2  13924  bdssex  14842