Definition df-ot 4576

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

This definition is referenced by:  oteq1  4825  oteq2  4826  oteq3  4827  otex  5418  otth  5437  otthg  5438  otelxp  5675  otel3xp  5677  fnotovb  7419  ot1stg  7956  ot2ndg  7957  ot3rdg  7958  el2xptp  7988  el2xptp0  7989  frxp3  8101  ottpos  8186  wunot  10646  elhomai2  18001  homadmcd  18009  elmpst  35718  mpst123  35722  mpstrcl  35723  mppspstlem  35753  elmpps  35755  hdmap1val  42244  fnotaovb  47646  ovsng2  49334  setc1ohomfval  49968  setc1ocofval  49969  mndtcco  50060