Definition df-ss 2053

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2058. Other possible definitions are given by dfss3 2059, dfss4 2242, sspss 2145, ssequn1 2200, ssequn2 2203, sseqin2 2229, and ssdif0 2327.

Assertion

Ref	Expression
df-ss	|- (A (_ B <-> (A i^i 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 2047	. 2 wff A (_ B
4	1, 2	cin 2046	. . 3 class (A i^i B)
5	4, 1	wceq 956	. 2 wff (A i^i B) = A
6	3, 5	wb 146	1 wff (A (_ B <-> (A i^i B) = A)

This definition is referenced by:  dfss 2054  sseqin2 2229  ssin 2232  inabs 2239  ssex 2719  op1stb 2913  ordtri3or 2979  ssdmres 3381  curry1 4098  cncfmet 7890  remetba 7894  bcthlem9 7992  dmdsl3t 10227  atssmat 10290  dmdbr6at 10335

Copyright terms: Public domain