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 1567	1 wff ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩

This definition is referenced by:  oteq1  4848  oteq2  4849  oteq3  4850  otex  5445  otth  5464  otthg  5465  otelxp  5703  otel3xp  5705  fnotovb  7460  ot1stg  7996  ot2ndg  7997  ot3rdg  7998  el2xptp  8028  el2xptp0  8029  frxp3  8143  ottpos  8228  wunot  10704  elhomai2  18087  homadmcd  18095  elmpst  35923  mpst123  35927  mpstrcl  35928  mppspstlem  35958  elmpps  35960  hdmap1val  42457  fnotaovb  47819  ovsng2  49517  setc1ohomfval  50151  setc1ocofval  50152  mndtcco  50243