Definition df-ss 3170

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴 ⊆ 𝐴 (proved in ssid 3203). For a more traditional definition, but requiring a dummy variable, see dfss2 3172. Other possible definitions are given by dfss3 3173, ssequn1 3333, ssequn2 3336, and sseqin2 3382. (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  dfss1  3367  inabs  3395  dfrab3ss  3441  disjssun  3514  riinm  3989  rintm  4009  ssex  4170  op1stb  4513  op1stbg  4514  ssdmres  4968  resima2  4980  xpssres  4981  fnimaeq0  5379  f0rn0  5452  fnreseql  5672  tpostpos2  6323  tfrexlem  6392  ecinxp  6669  uzin  9634  iooval2  9990  minmax  11395  xrminmax  11430  2prm  12295  dfphi2  12388  ressbas2d  12746  ressval3d  12750  restid2  12919  lidlbas  14034  difopn  14344  restopnb  14417  cnrest2  14472  bdssex  15548