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 4450
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 4449 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4447 . . 3 class 𝐴, 𝐵
65, 3cop 4447 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1507 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
Colors of variables: wff setvar class
This definition is referenced by:  oteq1  4686  oteq2  4687  oteq3  4688  otex  5214  otth  5233  otthg  5234  otel3xp  5451  fnotovb  7025  ot1stg  7515  ot2ndg  7516  ot3rdg  7517  el2xptp  7547  el2xptp0  7548  ottpos  7705  wunot  9943  elhomai2  17152  homadmcd  17160  elmpst  32309  mpst123  32313  mpstrcl  32314  mppspstlem  32344  elmpps  32346  hdmap1val  38385  fnotaovb  42809
  Copyright terms: Public domain W3C validator