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

Definition df-ot 4038
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
2 cB . . 3
3 cC . . 3
41, 2, 3cotp 4037 . 2
51, 2cop 4035 . . 3
65, 3cop 4035 . 2
74, 6wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  oteq1  4226  oteq2  4227  oteq3  4228  otex  4717  otth  4734  otthg  4735  otel3xp  5040  fnotovb  6338  ot1stg  6814  ot2ndg  6815  ot3rdg  6816  el2xptp  6843  el2xptp0  6844  ottpos  6984  wunot  9122  elhomai2  15361  homadmcd  15369  el2wlkonotot0  24872  2wlkonotv  24877  elmpst  28896  mpst123  28900  mpstrcl  28901  mppspstlem  28931  elmpps  28933  fnotaovb  32283  hdmap1val  37526
  Copyright terms: Public domain W3C validator