Definition df-ot 4567

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

This definition is referenced by:  oteq1  4810  oteq2  4811  oteq3  4812  otex  5374  otth  5393  otthg  5394  otel3xp  5624  fnotovb  7305  ot1stg  7818  ot2ndg  7819  ot3rdg  7820  el2xptp  7850  el2xptp0  7851  ottpos  8023  wunot  10410  elhomai2  17665  homadmcd  17673  elmpst  33398  mpst123  33402  mpstrcl  33403  mppspstlem  33433  elmpps  33435  hdmap1val  39739  fnotaovb  44577  mndtchom  46257  mndtcco  46258