![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opeq12 | Structured version Visualization version GIF version |
Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) |
Ref | Expression |
---|---|
opeq12 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 4541 | . 2 ⊢ (𝐴 = 𝐶 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) | |
2 | opeq2 4542 | . 2 ⊢ (𝐵 = 𝐷 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) | |
3 | 1, 2 | sylan9eq 2802 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1620 〈cop 4315 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-rab 3047 df-v 3330 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-sn 4310 df-pr 4312 df-op 4316 |
This theorem is referenced by: opeq12i 4546 opeq12d 4549 cbvopab 4861 opth 5081 copsex2t 5093 copsex2g 5094 relop 5416 funopg 6071 fvn0ssdmfun 6501 fsn 6553 fnressn 6576 fmptsng 6586 fmptsnd 6587 tpres 6618 cbvoprab12 6882 eqopi 7357 f1o2ndf1 7441 tposoprab 7545 omeu 7822 brecop 7995 ecovcom 8008 ecovass 8009 ecovdi 8010 xpf1o 8275 addsrmo 10057 mulsrmo 10058 addsrpr 10059 mulsrpr 10060 addcnsr 10119 axcnre 10148 seqeq1 12969 opfi1uzind 13446 fsumcnv 14674 fprodcnv 14883 eucalgval2 15467 xpstopnlem1 21785 qustgplem 22096 finsumvtxdg2size 26627 brabgaf 29698 qqhval2 30306 brsegle 32492 finxpreclem3 33512 eqrelf 34313 dvnprodlem1 40633 funop1 41779 uspgrsprf1 42234 |
Copyright terms: Public domain | W3C validator |