| 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 4634 | . 2 class 〈𝐴, 𝐵, 𝐶〉 |
| 5 | 1, 2 | cop 4632 | . . 3 class 〈𝐴, 𝐵〉 |
| 6 | 5, 3 | cop 4632 | . 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 5470 otth 5489 otthg 5490 otelxp 5729 otel3xp 5731 fnotovb 7483 ot1stg 8028 ot2ndg 8029 ot3rdg 8030 el2xptp 8060 el2xptp0 8061 frxp3 8176 ottpos 8261 wunot 10763 elhomai2 18079 homadmcd 18087 elmpst 35541 mpst123 35545 mpstrcl 35546 mppspstlem 35576 elmpps 35578 hdmap1val 41800 fnotaovb 47210 mndtchom 49181 mndtcco 49182 |
| Copyright terms: Public domain | W3C validator |