MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ot Structured version   Visualization version   GIF version

Definition df-ot 4568
Description: Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.)
Assertion
Ref Expression
df-ot 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶

Detailed syntax breakdown of Definition df-ot
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
41, 2, 3cotp 4567 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4565 . . 3 class 𝐴, 𝐵
65, 3cop 4565 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1528 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
Colors of variables: wff setvar class
This definition is referenced by:  oteq1  4806  oteq2  4807  oteq3  4808  otex  5349  otth  5368  otthg  5369  otel3xp  5593  fnotovb  7195  ot1stg  7694  ot2ndg  7695  ot3rdg  7696  el2xptp  7726  el2xptp0  7727  ottpos  7893  wunot  10134  elhomai2  17284  homadmcd  17292  elmpst  32681  mpst123  32685  mpstrcl  32686  mppspstlem  32716  elmpps  32718  hdmap1val  38816  fnotaovb  43278
  Copyright terms: Public domain W3C validator