Definition df-ot 4598

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

This definition is referenced by:  oteq1  4846  oteq2  4847  oteq3  4848  otex  5425  otth  5444  otthg  5445  otelxp  5682  otel3xp  5684  fnotovb  7439  ot1stg  7982  ot2ndg  7983  ot3rdg  7984  el2xptp  8014  el2xptp0  8015  frxp3  8130  ottpos  8215  wunot  10676  elhomai2  17996  homadmcd  18004  elmpst  35523  mpst123  35527  mpstrcl  35528  mppspstlem  35558  elmpps  35560  hdmap1val  41792  fnotaovb  47199  ovsng2  48847  setc1ohomfval  49482  setc1ocofval  49483  mndtcco  49574