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 4567 | . 2 class 〈𝐴, 𝐵, 𝐶〉 |
5 | 1, 2 | cop 4565 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cop 4565 | . 2 class 〈〈𝐴, 𝐵〉, 𝐶〉 |
7 | 4, 6 | wceq 1528 | 1 wff 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 |
Colors of variables: wff setvar class |
This definition is referenced by: oteq1 4806 oteq2 4807 oteq3 4808 otex 5349 otth 5368 otthg 5369 otel3xp 5593 fnotovb 7195 ot1stg 7694 ot2ndg 7695 ot3rdg 7696 el2xptp 7726 el2xptp0 7727 ottpos 7893 wunot 10134 elhomai2 17284 homadmcd 17292 elmpst 32681 mpst123 32685 mpstrcl 32686 mppspstlem 32716 elmpps 32718 hdmap1val 38816 fnotaovb 43278 |
Copyright terms: Public domain | W3C validator |