Definition df-ss 2105

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2110. Other possible definitions are given by dfss3 2111, dfss4 2294, sspss 2197, ssequn1 2252, ssequn2 2255, sseqin2 2281, and ssdif0 2380.

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 2099	. 2 wff A (_ B
4	1, 2	cin 2098	. . 3 class (A i^i B)
5	4, 1	wceq 992	. 2 wff (A i^i B) = A
6	3, 5	wb 144	1 wff (A (_ B <-> (A i^i B) = A)

This definition is referenced by:  dfss 2106  sseqin2 2281  ssin 2284  inabs 2291  ssex 2793  ordtri3or 3007  op1stb 3136  ssdmres 3471  curry1 4193  curry2 4196  cncfmet 8116  remetba 8120  bcthlem9 8218  dmdsl3 10523  atssma 10587  dmdbr6ati 10632  isunscov 10796  imrescl 10807  subtopsin2 11067  basmetres 11416  elfiun 11421  topbnd 11460  opnbnd 11461  subspid 11478  subsubtop 11479  subcld 11480  cnsubsp2 11484  compfipin0 11493  connsub 11502  subtopmetlem 11505  fbunfip 11631  extbas1 11641  gapm 11784  cnimass 11949  cnss 11953  paste 11954  heiborlem11 12021

Copyright terms: Public domain