Definition df-ot 4219

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

This definition is referenced by:  oteq1  4442  oteq2  4443  oteq3  4444  otex  4963  otth  4982  otthg  4983  otel3xp  5187  fnotovb  6735  fnotovbOLD  6736  ot1stg  7224  ot2ndg  7225  ot3rdg  7226  el2xptp  7255  el2xptp0  7256  ottpos  7407  wunot  9583  elhomai2  16731  homadmcd  16739  elmpst  31559  mpst123  31563  mpstrcl  31564  mppspstlem  31594  elmpps  31596  hdmap1val  37405  fnotaovb  41599