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 4804 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 〈cop 4567 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 |
This theorem is referenced by: oteq1 4813 oteq2 4814 opth 5391 elsnxp 6194 cbvoprab2 7363 fvproj 7975 unxpdomlem1 9027 djulf1o 9670 djurf1o 9671 mulcanenq 10716 ax1rid 10917 axrnegex 10918 fseq1m1p1 13331 uzrdglem 13677 pfxswrd 14419 swrdccat 14448 swrdccat3blem 14452 cshw0 14507 cshwmodn 14508 s2prop 14620 s4prop 14623 fsum2dlem 15482 fprod2dlem 15690 ruclem1 15940 imasaddvallem 17240 iscatd2 17390 moni 17448 homadmcd 17757 curf1 17943 curf1cl 17946 curf2 17947 hofcl 17977 gsum2dlem2 19572 imasdsf1olem 23526 ovoliunlem1 24666 cxpcn3 25901 axlowdimlem15 27324 axlowdim 27329 nvi 28976 nvop 29038 phop 29180 br8d 30950 fgreu 31009 1stpreimas 31038 smatfval 31745 smatrcl 31746 smatlem 31747 fmla0xp 33345 mvhfval 33495 mpst123 33502 br8 33723 frxp3 33797 xpord3pred 33798 nosupbnd2 33919 noinfbnd2 33934 fvtransport 34334 bj-inftyexpitaudisj 35376 rfovcnvf1od 41612 |
Copyright terms: Public domain | W3C validator |