Definition df-ot 4635

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

This definition is referenced by:  oteq1  4882  oteq2  4883  oteq3  4884  otex  5470  otth  5489  otthg  5490  otelxp  5729  otel3xp  5731  fnotovb  7483  ot1stg  8028  ot2ndg  8029  ot3rdg  8030  el2xptp  8060  el2xptp0  8061  frxp3  8176  ottpos  8261  wunot  10763  elhomai2  18079  homadmcd  18087  elmpst  35541  mpst123  35545  mpstrcl  35546  mppspstlem  35576  elmpps  35578  hdmap1val  41800  fnotaovb  47210  mndtchom  49181  mndtcco  49182