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

Definition df-ot 4219
 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 4218 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4216 . . 3 class 𝐴, 𝐵
65, 3cop 4216 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1523 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
 Colors of variables: wff setvar class This definition is referenced by:  oteq1  4442  oteq2  4443  oteq3  4444  otex  4963  otth  4982  otthg  4983  otel3xp  5187  fnotovb  6735  fnotovbOLD  6736  ot1stg  7224  ot2ndg  7225  ot3rdg  7226  el2xptp  7255  el2xptp0  7256  ottpos  7407  wunot  9583  elhomai2  16731  homadmcd  16739  elmpst  31559  mpst123  31563  mpstrcl  31564  mppspstlem  31594  elmpps  31596  hdmap1val  37405  fnotaovb  41599
 Copyright terms: Public domain W3C validator