Definition df-ot 4638

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

This definition is referenced by:  oteq1  4883  oteq2  4884  oteq3  4885  otex  5466  otth  5485  otthg  5486  otelxp  5721  otel3xp  5723  fnotovb  7459  ot1stg  7989  ot2ndg  7990  ot3rdg  7991  el2xptp  8021  el2xptp0  8022  frxp3  8137  ottpos  8221  wunot  10718  elhomai2  17984  homadmcd  17992  elmpst  34527  mpst123  34531  mpstrcl  34532  mppspstlem  34562  elmpps  34564  hdmap1val  40669  fnotaovb  45906  mndtchom  47710  mndtcco  47711