Definition df-ot 4570

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

This definition is referenced by:  oteq1  4813  oteq2  4814  oteq3  4815  otex  5380  otth  5399  otthg  5400  otel3xp  5633  fnotovb  7325  ot1stg  7845  ot2ndg  7846  ot3rdg  7847  el2xptp  7877  el2xptp0  7878  ottpos  8052  wunot  10479  elhomai2  17749  homadmcd  17757  elmpst  33498  mpst123  33502  mpstrcl  33503  mppspstlem  33533  elmpps  33535  hdmap1val  39812  fnotaovb  44690  mndtchom  46371  mndtcco  46372