Definition df-ot 4450

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 4449	. 2 class ⟨𝐴, 𝐵, 𝐶⟩
5	1, 2	cop 4447	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	cop 4447	. 2 class ⟨⟨𝐴, 𝐵⟩, 𝐶⟩
7	4, 6	wceq 1507	1 wff ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩

This definition is referenced by:  oteq1  4686  oteq2  4687  oteq3  4688  otex  5214  otth  5233  otthg  5234  otel3xp  5451  fnotovb  7025  ot1stg  7515  ot2ndg  7516  ot3rdg  7517  el2xptp  7547  el2xptp0  7548  ottpos  7705  wunot  9943  elhomai2  17152  homadmcd  17160  elmpst  32309  mpst123  32313  mpstrcl  32314  mppspstlem  32344  elmpps  32346  hdmap1val  38385  fnotaovb  42809