Definition df-ss 2868

Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2873. Other possible definitions are given by dfss3 2874, dfss4 3070, sspss 2963, ssequn1 3021, ssequn2 3024, sseqin2 3057, and ssdif0 3167.

Assertion

Ref	Expression
df-ss	|- (A C_ 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 2859	. 2 wff A C_ B
4	1, 2	cin 2858	. . 3 class (A i^i B)
5	4, 1	wceq 1615	. 2 wff (A i^i B) = A
6	3, 5	wb 231	1 wff (A C_ B <-> (A i^i B) = A)

This definition is referenced by:  dfss 2869  sseqin2 3057  inabs 3067  nssinpss 3068  disjssun 3166  ssex 3654  ordtri3or 3875  op1stb 4035  ssdmres 4389  curry1 5238  curry2 5241  cdainf 6325  cncfmet 10199  remetba 10203  bcthlem9 10303  gapm 10483  basmetres 11176  subspid 11243  subcld 11250  subtopmetlem 11251  fbunfip 11278  extbas1 11287  dmdsl3 12876  atssma 12939  dmdbr6ati 12984  bnj1322 13984  dmaddnq 14551  dmmulnq 14552  dfon2lem4 14733  sspred 14774  axdense 14943  dfiota3 15024  dfoprab4spop 15308  isunscov 15357  imrescl 15364  nZdef 15527  domrancur1b 15548  domrancur1c 15550  subtopsin2 15930  subtopsin2OLD 15931  valdom 16332  elfiun 16454  topbnd 16493  opnbnd 16494  subsubtop 16508  cnsubsp2 16512  compfipin0 16521  connsub 16528  cnimass 16973  cnss 16977  paste 16978  heiborlem11 17050

Copyright terms: Public domain