Definition df-ot 4588

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

This definition is referenced by:  oteq1  4837  oteq2  4838  oteq3  4839  otex  5430  otth  5449  otthg  5450  otelxp  5687  otel3xp  5689  fnotovb  7443  ot1stg  7979  ot2ndg  7980  ot3rdg  7981  el2xptp  8011  el2xptp0  8012  frxp3  8125  ottpos  8210  wunot  10675  elhomai2  18058  homadmcd  18066  elmpst  35847  mpst123  35851  mpstrcl  35852  mppspstlem  35882  elmpps  35884  hdmap1val  42383  fnotaovb  47753  ovsng2  49441  setc1ohomfval  50075  setc1ocofval  50076  mndtcco  50167