![]() |
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 4449 | . 2 class 〈𝐴, 𝐵, 𝐶〉 |
5 | 1, 2 | cop 4447 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cop 4447 | . 2 class 〈〈𝐴, 𝐵〉, 𝐶〉 |
7 | 4, 6 | wceq 1507 | 1 wff 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 |
Colors of variables: wff setvar class |
This definition is referenced by: oteq1 4686 oteq2 4687 oteq3 4688 otex 5214 otth 5233 otthg 5234 otel3xp 5451 fnotovb 7025 ot1stg 7515 ot2ndg 7516 ot3rdg 7517 el2xptp 7547 el2xptp0 7548 ottpos 7705 wunot 9943 elhomai2 17152 homadmcd 17160 elmpst 32309 mpst123 32313 mpstrcl 32314 mppspstlem 32344 elmpps 32346 hdmap1val 38385 fnotaovb 42809 |
Copyright terms: Public domain | W3C validator |