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 4379
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 4378 . 2 class 𝐴, 𝐵, 𝐶
51, 2cop 4376 . . 3 class 𝐴, 𝐵
65, 3cop 4376 . 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶
74, 6wceq 1637 1 wff 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
Colors of variables: wff setvar class
This definition is referenced by:  oteq1  4604  oteq2  4605  oteq3  4606  otex  5123  otth  5142  otthg  5143  otel3xp  5353  fnotovb  6923  fnotovbOLD  6924  ot1stg  7412  ot2ndg  7413  ot3rdg  7414  el2xptp  7443  el2xptp0  7444  ottpos  7597  wunot  9830  elhomai2  16888  homadmcd  16896  elmpst  31756  mpst123  31760  mpstrcl  31761  mppspstlem  31791  elmpps  31793  hdmap1val  37579  fnotaovb  41787
  Copyright terms: Public domain W3C validator