Definition df-ot 4864

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

This definition is used by:  oteq1  4865  oteq2  4866  oteq3  4867  otex  5441  otth  5460  otthg  5461  otelxp  5702  otel3xp  5704  el2xptp  5830  fnotovb  7503  ot1stg  8049  ot2ndg  8050  ot3rdg  8051  el2xptp0  8081  frxp3  8205  ottpos  8291  wunot  10847  elhomai2  18259  homadmcd  18267  ot1st2nd  35836  dfj2  36050  elmpst  36509  mpst123  36513  mpstrcl  36514  mppspstlem  36544  elmpps  36546  hdmap1val  43121  fnotaovb  48541  ovsng2  50301  setc1ohomfval  50959  setc1ocofval  50960  mndtcco  51054