Definition df-ot 4577

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

This definition is referenced by:  oteq1  4826  oteq2  4827  oteq3  4828  otex  5413  otth  5432  otthg  5433  otelxp  5668  otel3xp  5670  fnotovb  7412  ot1stg  7949  ot2ndg  7950  ot3rdg  7951  el2xptp  7981  el2xptp0  7982  frxp3  8094  ottpos  8179  wunot  10637  elhomai2  17992  homadmcd  18000  elmpst  35734  mpst123  35738  mpstrcl  35739  mppspstlem  35769  elmpps  35771  hdmap1val  42258  fnotaovb  47658  ovsng2  49346  setc1ohomfval  49980  setc1ocofval  49981  mndtcco  50072