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 4784 | . 2 ⊢ (𝐴 = 𝐶 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) | |
2 | opeq2 4785 | . 2 ⊢ (𝐵 = 𝐷 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) | |
3 | 1, 2 | sylan9eq 2798 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 〈cop 4547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 |
This theorem is referenced by: opeq12i 4789 opeq12d 4792 cbvopab 5125 cbvopabv 5126 opth 5360 copsex2t 5375 copsex2gOLD 5377 relop 5719 funopg 6414 fvn0ssdmfun 6895 fsn 6950 fnressn 6973 fmptsng 6983 fmptsnd 6984 tpres 7016 cbvoprab12 7300 eqopi 7797 f1o2ndf1 7891 tposoprab 8004 omeu 8313 brecop 8492 ecovcom 8505 ecovass 8506 ecovdi 8507 xpf1o 8808 addsrmo 10687 mulsrmo 10688 addsrpr 10689 mulsrpr 10690 addcnsr 10749 axcnre 10778 seqeq1 13577 opfi1uzind 14067 fsumcnv 15337 fprodcnv 15545 eucalgval2 16138 xpstopnlem1 22706 qustgplem 23018 finsumvtxdg2size 27638 brabgaf 30667 qqhval2 31644 brsegle 34147 copsex2d 35045 finxpreclem3 35301 eqrelf 36132 dvnprodlem1 43162 or2expropbilem1 44198 or2expropbilem2 44199 funop1 44447 ich2exprop 44596 ichnreuop 44597 ichreuopeq 44598 reuopreuprim 44651 uspgrsprf1 44982 |
Copyright terms: Public domain | W3C validator |