Definition df-ot 4585

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

This definition is referenced by:  oteq1  4834  oteq2  4835  oteq3  4836  otex  5405  otth  5424  otthg  5425  otelxp  5660  otel3xp  5662  fnotovb  7398  ot1stg  7935  ot2ndg  7936  ot3rdg  7937  el2xptp  7967  el2xptp0  7968  frxp3  8081  ottpos  8166  wunot  10611  elhomai2  17938  homadmcd  17946  elmpst  35568  mpst123  35572  mpstrcl  35573  mppspstlem  35603  elmpps  35605  hdmap1val  41836  fnotaovb  47228  ovsng2  48889  setc1ohomfval  49524  setc1ocofval  49525  mndtcco  49616