Definition df-ot 4186

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

This definition is referenced by:  oteq1  4411  oteq2  4412  oteq3  4413  otex  4933  otth  4953  otthg  4954  otel3xp  5153  fnotovb  6694  ot1stg  7182  ot2ndg  7183  ot3rdg  7184  el2xptp  7211  el2xptp0  7212  ottpos  7362  wunot  9545  elhomai2  16684  homadmcd  16692  elmpst  31433  mpst123  31437  mpstrcl  31438  mppspstlem  31468  elmpps  31470  hdmap1val  37088  fnotaovb  41278