HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-ss 2043
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2048. Other possible definitions are given by dfss3 2049, dfss4 2232, sspss 2135, ssequn1 2190, ssequn2 2193, sseqin2 2219, and ssdif0 2317.
Assertion
Ref Expression
df-ss |- (A (_ B <-> (A i^i B) = A)
Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2wss 2037 . 2 wff A (_ B
41, 2cin 2036 . . 3 class (A i^i B)
54, 1wceq 953 . 2 wff (A i^i B) = A
63, 5wb 146 1 wff (A (_ B <-> (A i^i B) = A)
Colors of variables: wff set class
This definition is referenced by:  dfss 2044  sseqin2 2219  ssin 2222  inabs 2229  ssex 2709  op1stb 2903  ordtri3or 2969  ssdmres 3365  curry1 4082  cncfmet 7844  remetba 7848  bcthlem9 7941  dmdsl3t 10150  atssmat 10213  dmdbr6at 10256
Copyright terms: Public domain