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

Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3		cC	. . 3
4	1, 2, 3	cotp 4037	. 2
5	1, 2	cop 4035	. . 3
6	5, 3	cop 4035	. 2
7	4, 6	wceq 1395	1

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