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  3477  riinm  3943  rintm  3963  ssex  4124  op1stb  4461  op1stbg  4462  ssdmres  4911  resima2  4923  xpssres  4924  fnimaeq0  5317  f0rn0  5390  fnreseql  5604  tpostpos2  6242  tfrexlem  6311  ecinxp  6585  uzin  9508  iooval2  9861  minmax  11182  xrminmax  11217  2prm  12070  dfphi2  12163  restid2  12577  difopn  12863  restopnb  12936  cnrest2  12991  bdssex  13899