Definition df-ot 4593

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

This definition is used by:  oteq1  4842  oteq2  4843  oteq3  4844  otex  5434  otth  5453  otthg  5454  otelxp  5695  otel3xp  5697  el2xptp  5820  fnotovb  7470  ot1stg  8013  ot2ndg  8014  ot3rdg  8015  el2xptp0  8045  frxp3  8161  ottpos  8246  wunot  10801  elhomai2  18202  homadmcd  18210  elmpst  36280  mpst123  36284  mpstrcl  36285  mppspstlem  36315  elmpps  36317  hdmap1val  42835  fnotaovb  48237  ovsng2  49938  setc1ohomfval  50570  setc1ocofval  50571  mndtcco  50662