Definition df-ot 4657

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

This definition is referenced by:  oteq1  4906  oteq2  4907  oteq3  4908  otex  5485  otth  5504  otthg  5505  otelxp  5744  otel3xp  5746  fnotovb  7500  ot1stg  8044  ot2ndg  8045  ot3rdg  8046  el2xptp  8076  el2xptp0  8077  frxp3  8192  ottpos  8277  wunot  10792  elhomai2  18101  homadmcd  18109  elmpst  35504  mpst123  35508  mpstrcl  35509  mppspstlem  35539  elmpps  35541  hdmap1val  41755  fnotaovb  47113  mndtchom  48757  mndtcco  48758