Definition df-ot 4134

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

This definition is referenced by:  oteq1  4349  oteq2  4350  oteq3  4351  otex  4860  otth  4879  otthg  4880  otel3xp  5077  fnotovb  6592  ot1stg  7073  ot2ndg  7074  ot3rdg  7075  el2xptp  7102  el2xptp0  7103  ottpos  7249  wunot  9424  elhomai2  16507  homadmcd  16515  el2wlkonotot0  26399  2wlkonotv  26404  elmpst  30687  mpst123  30691  mpstrcl  30692  mppspstlem  30722  elmpps  30724  hdmap1val  36106  fnotaovb  39927