Definition df-ot 4591

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

This definition is referenced by:  oteq1  4840  oteq2  4841  oteq3  4842  otex  5421  otth  5440  otthg  5441  otelxp  5676  otel3xp  5678  fnotovb  7420  ot1stg  7957  ot2ndg  7958  ot3rdg  7959  el2xptp  7989  el2xptp0  7990  frxp3  8103  ottpos  8188  wunot  10646  elhomai2  17970  homadmcd  17978  elmpst  35752  mpst123  35756  mpstrcl  35757  mppspstlem  35787  elmpps  35789  hdmap1val  42174  fnotaovb  47558  ovsng2  49218  setc1ohomfval  49852  setc1ocofval  49853  mndtcco  49944