Definition df-ot 4536

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

This definition is referenced by:  oteq1  4779  oteq2  4780  oteq3  4781  otex  5334  otth  5353  otthg  5354  otel3xp  5580  fnotovb  7241  ot1stg  7753  ot2ndg  7754  ot3rdg  7755  el2xptp  7785  el2xptp0  7786  ottpos  7956  wunot  10302  elhomai2  17494  homadmcd  17502  elmpst  33165  mpst123  33169  mpstrcl  33170  mppspstlem  33200  elmpps  33202  hdmap1val  39498  fnotaovb  44305  mndtchom  45985  mndtcco  45986