Definition df-ot 4589

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

This definition is referenced by:  oteq1  4838  oteq2  4839  oteq3  4840  otex  5413  otth  5432  otthg  5433  otelxp  5668  otel3xp  5670  fnotovb  7410  ot1stg  7947  ot2ndg  7948  ot3rdg  7949  el2xptp  7979  el2xptp0  7980  frxp3  8093  ottpos  8178  wunot  10634  elhomai2  17958  homadmcd  17966  elmpst  35730  mpst123  35734  mpstrcl  35735  mppspstlem  35765  elmpps  35767  hdmap1val  42058  fnotaovb  47444  ovsng2  49104  setc1ohomfval  49738  setc1ocofval  49739  mndtcco  49830