Definition df-ot 4600

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

This definition is used by:  oteq1  4849  oteq2  4850  oteq3  4851  otex  5449  otth  5468  otthg  5469  otelxp  5707  otel3xp  5709  fnotovb  7471  ot1stg  8006  ot2ndg  8007  ot3rdg  8008  el2xptp  8038  el2xptp0  8039  frxp3  8153  ottpos  8238  wunot  10723  elhomai2  18113  homadmcd  18121  elmpst  36065  mpst123  36069  mpstrcl  36070  mppspstlem  36100  elmpps  36102  hdmap1val  42630  fnotaovb  47993  ovsng2  49694  setc1ohomfval  50328  setc1ocofval  50329  mndtcco  50420