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

Definition df-ot 4534
 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 4533 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4531 . . 3 class 𝐴, 𝐵
65, 3cop 4531 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1538 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
 Colors of variables: wff setvar class This definition is referenced by:  oteq1  4774  oteq2  4775  oteq3  4776  otex  5322  otth  5341  otthg  5342  otel3xp  5563  fnotovb  7185  ot1stg  7685  ot2ndg  7686  ot3rdg  7687  el2xptp  7717  el2xptp0  7718  ottpos  7885  wunot  10134  elhomai2  17286  homadmcd  17294  elmpst  32893  mpst123  32897  mpstrcl  32898  mppspstlem  32928  elmpps  32930  hdmap1val  39091  fnotaovb  43749
 Copyright terms: Public domain W3C validator