Definition df-ot 4639

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

This definition is referenced by:  oteq1  4886  oteq2  4887  oteq3  4888  otex  5475  otth  5494  otthg  5495  otelxp  5732  otel3xp  5734  fnotovb  7482  ot1stg  8026  ot2ndg  8027  ot3rdg  8028  el2xptp  8058  el2xptp0  8059  frxp3  8174  ottpos  8259  wunot  10760  elhomai2  18087  homadmcd  18095  elmpst  35520  mpst123  35524  mpstrcl  35525  mppspstlem  35555  elmpps  35557  hdmap1val  41780  fnotaovb  47147  mndtchom  48892  mndtcco  48893