![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-ot | Structured version Visualization version GIF version |
Description: Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
Ref | Expression |
---|---|
df-ot | ⊢ 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cC | . . 3 class 𝐶 | |
4 | 1, 2, 3 | cotp 4636 | . 2 class 〈𝐴, 𝐵, 𝐶〉 |
5 | 1, 2 | cop 4634 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cop 4634 | . 2 class 〈〈𝐴, 𝐵〉, 𝐶〉 |
7 | 4, 6 | wceq 1540 | 1 wff 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 |
Colors of variables: wff setvar class |
This definition is referenced by: oteq1 4882 oteq2 4883 oteq3 4884 otex 5465 otth 5484 otthg 5485 otelxp 5720 otel3xp 5722 fnotovb 7462 ot1stg 7993 ot2ndg 7994 ot3rdg 7995 el2xptp 8025 el2xptp0 8026 frxp3 8142 ottpos 8227 wunot 10724 elhomai2 17994 homadmcd 18002 elmpst 34993 mpst123 34997 mpstrcl 34998 mppspstlem 35028 elmpps 35030 hdmap1val 41136 fnotaovb 46368 mndtchom 47875 mndtcco 47876 |
Copyright terms: Public domain | W3C validator |