Definition df-ss 2024

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2029. Other possible definitions are given by dfss3 2030, dfss4 2213, sspss 2116, ssequn1 2171, ssequn2 2174, sseqin2 2200, and ssdif0 2298.

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 2018	. 2 wff A (_ B
4	1, 2	cin 2017	. . 3 class (A i^i B)
5	4, 1	wceq 1099	. 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 2025  sseqin2 2200  ssin 2203  inabs 2210  ssex 2687  op1stb 2876  ordtri3or 2942  ssdmres 3332  curry1 4036  cncfmet 7792  remetba 7796  bcthlem9 7889  dmdsl3t 10364  atssmat 10427  dmdbr6at 10470

Copyright terms: Public domain