Definition df-ot 4858

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

This definition is used by:  oteq1  4859  oteq2  4860  oteq3  4861  otex  5434  otth  5453  otthg  5454  otelxp  5695  otel3xp  5697  el2xptp  5821  fnotovb  7476  ot1stg  8019  ot2ndg  8020  ot3rdg  8021  el2xptp0  8051  frxp3  8174  ottpos  8260  wunot  10815  elhomai2  18218  homadmcd  18226  elmpst  36391  mpst123  36395  mpstrcl  36396  mppspstlem  36426  elmpps  36428  hdmap1val  42964  fnotaovb  48376  ovsng2  50078  setc1ohomfval  50736  setc1ocofval  50737  mndtcco  50831