Definition df-ot 4588

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

This definition is referenced by:  oteq1  4836  oteq2  4837  oteq3  4838  otex  5412  otth  5431  otthg  5432  otelxp  5667  otel3xp  5669  fnotovb  7405  ot1stg  7945  ot2ndg  7946  ot3rdg  7947  el2xptp  7977  el2xptp0  7978  frxp3  8091  ottpos  8176  wunot  10636  elhomai2  17959  homadmcd  17967  elmpst  35508  mpst123  35512  mpstrcl  35513  mppspstlem  35543  elmpps  35545  hdmap1val  41777  fnotaovb  47183  ovsng2  48844  setc1ohomfval  49479  setc1ocofval  49480  mndtcco  49571