![]() |
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 4671 | . 2 ⊢ (𝐴 = 𝐶 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) | |
2 | opeq2 4672 | . 2 ⊢ (𝐵 = 𝐷 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) | |
3 | 1, 2 | sylan9eq 2828 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 〈cop 4441 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 |
This theorem is referenced by: opeq12i 4676 opeq12d 4679 cbvopab 4994 opth 5219 copsex2t 5233 copsex2g 5234 relop 5565 funopg 6216 fvn0ssdmfun 6661 fsn 6714 fnressn 6737 fmptsng 6747 fmptsnd 6748 tpres 6784 cbvoprab12 7053 eqopi 7531 f1o2ndf1 7617 tposoprab 7725 omeu 8006 brecop 8184 ecovcom 8197 ecovass 8198 ecovdi 8199 xpf1o 8469 addsrmo 10287 mulsrmo 10288 addsrpr 10289 mulsrpr 10290 addcnsr 10349 axcnre 10378 seqeq1 13181 opfi1uzind 13664 fsumcnv 14982 fprodcnv 15191 eucalgval2 15775 xpstopnlem1 22115 qustgplem 22426 finsumvtxdg2size 27029 brabgaf 30117 qqhval2 30867 brsegle 33090 finxpreclem3 34115 eqrelf 34961 dvnprodlem1 41661 or2expropbilem1 42672 or2expropbilem2 42673 funop1 42888 ich2exprop 43001 ichnreuop 43002 ichreuopeq 43003 reuopreuprim 43056 uspgrsprf1 43390 |
Copyright terms: Public domain | W3C validator |