![]() |
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 4875 | . 2 ⊢ (𝐴 = 𝐶 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) | |
2 | opeq2 4876 | . 2 ⊢ (𝐵 = 𝐷 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) | |
3 | 1, 2 | sylan9eq 2785 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 〈cop 4636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 |
This theorem is referenced by: opeq12i 4880 opeq12d 4883 cbvopab 5221 cbvopabv 5222 opth 5478 copsex2t 5494 copsex2gOLD 5496 relop 5853 funopg 6588 fvn0ssdmfun 7083 fsn 7144 fnressn 7167 fmptsng 7177 fmptsnd 7178 tpres 7213 cbvoprab12 7509 eqopi 8030 f1o2ndf1 8127 tposoprab 8268 omeu 8606 brecop 8829 ecovcom 8842 ecovass 8843 ecovdi 8844 xpf1o 9167 addsrmo 11103 mulsrmo 11104 addsrpr 11105 mulsrpr 11106 addcnsr 11165 axcnre 11194 seqeq1 14010 opfi1uzind 14503 fsumcnv 15760 fprodcnv 15968 eucalgval2 16560 xpstopnlem1 23762 qustgplem 24074 finsumvtxdg2size 29441 brabgaf 32482 qqhval2 33716 brsegle 35837 copsex2d 36751 finxpreclem3 37005 eqrelf 37859 dvnprodlem1 45474 or2expropbilem1 46554 or2expropbilem2 46555 funop1 46803 ich2exprop 46950 ichnreuop 46951 ichreuopeq 46952 reuopreuprim 47005 uspgrsprf1 47397 |
Copyright terms: Public domain | W3C validator |