Definition df-ot 4598

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

This definition is referenced by:  oteq1  4847  oteq2  4848  oteq3  4849  otex  5447  otth  5466  otthg  5467  otelxp  5705  otel3xp  5707  fnotovb  7462  ot1stg  7996  ot2ndg  7997  ot3rdg  7998  el2xptp  8028  el2xptp0  8029  frxp3  8143  ottpos  8228  wunot  10703  elhomai2  18086  homadmcd  18094  elmpst  36028  mpst123  36032  mpstrcl  36033  mppspstlem  36063  elmpps  36065  hdmap1val  42572  fnotaovb  47935  ovsng2  49637  setc1ohomfval  50271  setc1ocofval  50272  mndtcco  50363