Definition df-ot 4610

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

This definition is referenced by:  oteq1  4858  oteq2  4859  oteq3  4860  otex  5440  otth  5459  otthg  5460  otelxp  5698  otel3xp  5700  fnotovb  7455  ot1stg  8000  ot2ndg  8001  ot3rdg  8002  el2xptp  8032  el2xptp0  8033  frxp3  8148  ottpos  8233  wunot  10735  elhomai2  18045  homadmcd  18053  elmpst  35504  mpst123  35508  mpstrcl  35509  mppspstlem  35539  elmpps  35541  hdmap1val  41763  fnotaovb  47175  ovsng2  48783  setc1ohomfval  49326  setc1ocofval  49327  mndtcco  49410