Definition df-ot 4636

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

This definition is referenced by:  oteq1  4881  oteq2  4882  oteq3  4883  otex  5464  otth  5483  otthg  5484  otelxp  5718  otel3xp  5720  fnotovb  7454  ot1stg  7984  ot2ndg  7985  ot3rdg  7986  el2xptp  8016  el2xptp0  8017  frxp3  8132  ottpos  8216  wunot  10714  elhomai2  17980  homadmcd  17988  elmpst  34465  mpst123  34469  mpstrcl  34470  mppspstlem  34500  elmpps  34502  hdmap1val  40607  fnotaovb  45841  mndtchom  47612  mndtcco  47613