Definition df-ot 4637

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

This definition is referenced by:  oteq1  4882  oteq2  4883  oteq3  4884  otex  5465  otth  5484  otthg  5485  otelxp  5720  otel3xp  5722  fnotovb  7462  ot1stg  7993  ot2ndg  7994  ot3rdg  7995  el2xptp  8025  el2xptp0  8026  frxp3  8142  ottpos  8227  wunot  10724  elhomai2  17994  homadmcd  18002  elmpst  34993  mpst123  34997  mpstrcl  34998  mppspstlem  35028  elmpps  35030  hdmap1val  41136  fnotaovb  46368  mndtchom  47875  mndtcco  47876