Definition df-ot 4584

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

This definition is referenced by:  oteq1  4833  oteq2  4834  oteq3  4835  otex  5408  otth  5427  otthg  5428  otelxp  5663  otel3xp  5665  fnotovb  7404  ot1stg  7941  ot2ndg  7942  ot3rdg  7943  el2xptp  7973  el2xptp0  7974  frxp3  8087  ottpos  8172  wunot  10621  elhomai2  17943  homadmcd  17951  elmpst  35601  mpst123  35605  mpstrcl  35606  mppspstlem  35636  elmpps  35638  hdmap1val  41917  fnotaovb  47322  ovsng2  48983  setc1ohomfval  49618  setc1ocofval  49619  mndtcco  49710