Definition df-ss 2049

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2054. Other possible definitions are given by dfss3 2055, dfss4 2238, sspss 2141, ssequn1 2196, ssequn2 2199, sseqin2 2225, and ssdif0 2323.

Assertion

Ref	Expression
df-ss	⊢ (A ⊆ B ↔ (A ∩ B) = A)

Detailed syntax breakdown of Definition df-ss

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wss 2043	. 2 wff A ⊆ B
4	1, 2	cin 2042	. . 3 class (A ∩ B)
5	4, 1	wceq 954	. 2 wff (A ∩ B) = A
6	3, 5	wb 146	1 wff (A ⊆ B ↔ (A ∩ B) = A)

This definition is referenced by:  dfss 2050  sseqin2 2225  ssin 2228  inabs 2235  ssex 2715  op1stb 2912  ordtri3or 2978  ordtri3orOLD 2979  ssdmres 3379  curry1 4099  cncfmet 7869  remetba 7873  bcthlem9 7969  dmdsl3t 10213  atssmat 10276  dmdbr6at 10319

Copyright terms: Public domain