Definition df-ot 4593

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

This definition is used by:  oteq1  4842  oteq2  4843  oteq3  4844  otex  5441  otth  5460  otthg  5461  otelxp  5699  otel3xp  5701  fnotovb  7465  ot1stg  8000  ot2ndg  8001  ot3rdg  8002  el2xptp  8032  el2xptp0  8033  frxp3  8149  ottpos  8234  wunot  10732  elhomai2  18123  homadmcd  18131  elmpst  36115  mpst123  36119  mpstrcl  36120  mppspstlem  36150  elmpps  36152  hdmap1val  42671  fnotaovb  48086  ovsng2  49787  setc1ohomfval  50419  setc1ocofval  50420  mndtcco  50511