Definition df-ot 4576

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 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4	1, 2, 3	cotp 4575	. 2 class ⟨𝐴, 𝐵, 𝐶⟩
5	1, 2	cop 4573	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cop 4573	. 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶⟩
7	4, 6	wceq 1537	1 wff ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩

This definition is referenced by:  oteq1  4812  oteq2  4813  oteq3  4814  otex  5357  otth  5376  otthg  5377  otel3xp  5599  fnotovb  7206  ot1stg  7703  ot2ndg  7704  ot3rdg  7705  el2xptp  7735  el2xptp0  7736  ottpos  7902  wunot  10145  elhomai2  17294  homadmcd  17302  elmpst  32783  mpst123  32787  mpstrcl  32788  mppspstlem  32818  elmpps  32820  hdmap1val  38949  fnotaovb  43417