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 4635
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 4634 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4632 . . 3 class 𝐴, 𝐵
65, 3cop 4632 . 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  5470  otth  5489  otthg  5490  otelxp  5729  otel3xp  5731  fnotovb  7483  ot1stg  8028  ot2ndg  8029  ot3rdg  8030  el2xptp  8060  el2xptp0  8061  frxp3  8176  ottpos  8261  wunot  10763  elhomai2  18079  homadmcd  18087  elmpst  35541  mpst123  35545  mpstrcl  35546  mppspstlem  35576  elmpps  35578  hdmap1val  41800  fnotaovb  47210  mndtchom  49181  mndtcco  49182
  Copyright terms: Public domain W3C validator