![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
Ref | Expression |
---|---|
opeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
opeq1d | ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | opeq1 4433 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 〈cop 4216 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 |
This theorem is referenced by: oteq1 4442 oteq2 4443 opth 4974 elsnxp 5715 cbvoprab2 6770 unxpdomlem1 8205 mulcanenq 9820 ax1rid 10020 axrnegex 10021 fseq1m1p1 12453 uzrdglem 12796 swrd0swrd 13507 swrdccat 13539 swrdccat3a 13540 swrdccat3blem 13541 cshw0 13586 cshwmodn 13587 s2prop 13698 s4prop 13701 fsum2dlem 14545 fprod2dlem 14754 ruclem1 15004 imasaddvallem 16236 iscatd2 16389 moni 16443 homadmcd 16739 curf1 16912 curf1cl 16915 curf2 16916 hofcl 16946 gsum2dlem2 18416 imasdsf1olem 22225 ovoliunlem1 23316 cxpcn3 24534 axlowdimlem15 25881 axlowdim 25886 nvi 27597 nvop 27659 phop 27801 br8d 29548 fgreu 29599 1stpreimas 29611 smatfval 29989 smatrcl 29990 smatlem 29991 fvproj 30027 mvhfval 31556 mpst123 31563 br8 31772 nosupbnd2 31987 fvtransport 32264 rfovcnvf1od 38615 |
Copyright terms: Public domain | W3C validator |