![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opeq12i | Structured version Visualization version GIF version |
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
opeq1i.1 | ⊢ 𝐴 = 𝐵 |
opeq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
opeq12i | ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | opeq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
3 | opeq12 4767 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 〈cop 4531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-sn 4526 df-pr 4528 df-op 4532 |
This theorem is referenced by: sbcop 5345 elxp6 7705 addcompq 10361 mulcompq 10363 addassnq 10369 mulassnq 10370 distrnq 10372 1lt2nq 10384 axi2m1 10570 om2uzrdg 13319 axlowdimlem6 26741 clwlkclwwlkflem 27789 konigsbergvtx 28031 konigsbergiedg 28032 nvop2 28391 nvvop 28392 phop 28601 hhsssh 29052 cshw1s2 30660 rngoi 35337 isdrngo1 35394 |
Copyright terms: Public domain | W3C validator |