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 4637
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 4636 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4634 . . 3 class 𝐴, 𝐵
65, 3cop 4634 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1540 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
Colors of variables: wff setvar class
This definition is referenced by:  oteq1  4882  oteq2  4883  oteq3  4884  otex  5465  otth  5484  otthg  5485  otelxp  5720  otel3xp  5722  fnotovb  7462  ot1stg  7993  ot2ndg  7994  ot3rdg  7995  el2xptp  8025  el2xptp0  8026  frxp3  8142  ottpos  8227  wunot  10724  elhomai2  17994  homadmcd  18002  elmpst  34993  mpst123  34997  mpstrcl  34998  mppspstlem  35028  elmpps  35030  hdmap1val  41136  fnotaovb  46368  mndtchom  47875  mndtcco  47876
  Copyright terms: Public domain W3C validator