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 4559
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 4558 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4556 . . 3 class 𝐴, 𝐵
65, 3cop 4556 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1543 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
Colors of variables: wff setvar class
This definition is referenced by:  oteq1  4802  oteq2  4803  oteq3  4804  otex  5358  otth  5377  otthg  5378  otel3xp  5604  fnotovb  7272  ot1stg  7784  ot2ndg  7785  ot3rdg  7786  el2xptp  7816  el2xptp0  7817  ottpos  7987  wunot  10350  elhomai2  17553  homadmcd  17561  elmpst  33224  mpst123  33228  mpstrcl  33229  mppspstlem  33259  elmpps  33261  hdmap1val  39562  fnotaovb  44377  mndtchom  46057  mndtcco  46058
  Copyright terms: Public domain W3C validator