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 4558 | . 2 class 〈𝐴, 𝐵, 𝐶〉 |
5 | 1, 2 | cop 4556 | . . 3 class 〈𝐴, 𝐵〉 |
6 | 5, 3 | cop 4556 | . 2 class 〈〈𝐴, 𝐵〉, 𝐶〉 |
7 | 4, 6 | wceq 1543 | 1 wff 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 |
Colors of variables: wff setvar class |
This definition is referenced by: oteq1 4802 oteq2 4803 oteq3 4804 otex 5358 otth 5377 otthg 5378 otel3xp 5604 fnotovb 7272 ot1stg 7784 ot2ndg 7785 ot3rdg 7786 el2xptp 7816 el2xptp0 7817 ottpos 7987 wunot 10350 elhomai2 17553 homadmcd 17561 elmpst 33224 mpst123 33228 mpstrcl 33229 mppspstlem 33259 elmpps 33261 hdmap1val 39562 fnotaovb 44377 mndtchom 46057 mndtcco 46058 |
Copyright terms: Public domain | W3C validator |