Definition df-ot 4564

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

This definition is referenced by:  oteq1  4813  oteq2  4814  oteq3  4815  otex  5405  otth  5424  otthg  5425  otelxp  5662  otel3xp  5664  fnotovb  7408  ot1stg  7945  ot2ndg  7946  ot3rdg  7947  el2xptp  7977  el2xptp0  7978  frxp3  8091  ottpos  8176  wunot  10637  elhomai2  17992  homadmcd  18000  elmpst  35764  mpst123  35768  mpstrcl  35769  mppspstlem  35799  elmpps  35801  hdmap1val  42290  fnotaovb  47661  ovsng2  49349  setc1ohomfval  49983  setc1ocofval  49984  mndtcco  50075