Definition df-ot 4601

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

This definition is referenced by:  oteq1  4849  oteq2  4850  oteq3  4851  otex  5428  otth  5447  otthg  5448  otelxp  5685  otel3xp  5687  fnotovb  7442  ot1stg  7985  ot2ndg  7986  ot3rdg  7987  el2xptp  8017  el2xptp0  8018  frxp3  8133  ottpos  8218  wunot  10683  elhomai2  18003  homadmcd  18011  elmpst  35530  mpst123  35534  mpstrcl  35535  mppspstlem  35565  elmpps  35567  hdmap1val  41799  fnotaovb  47203  ovsng2  48851  setc1ohomfval  49486  setc1ocofval  49487  mndtcco  49578