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 4756 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 〈cop 4519 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-un 3846 df-sn 4514 df-pr 4516 df-op 4520 |
This theorem is referenced by: oteq1 4767 oteq2 4768 opth 5331 elsnxp 6117 cbvoprab2 7250 fvproj 7847 unxpdomlem1 8794 djulf1o 9407 djurf1o 9408 mulcanenq 10453 ax1rid 10654 axrnegex 10655 fseq1m1p1 13066 uzrdglem 13409 pfxswrd 14150 swrdccat 14179 swrdccat3blem 14183 cshw0 14238 cshwmodn 14239 s2prop 14351 s4prop 14354 fsum2dlem 15211 fprod2dlem 15419 ruclem1 15669 imasaddvallem 16898 iscatd2 17048 moni 17104 homadmcd 17407 curf1 17584 curf1cl 17587 curf2 17588 hofcl 17618 gsum2dlem2 19203 imasdsf1olem 23119 ovoliunlem1 24247 cxpcn3 25481 axlowdimlem15 26894 axlowdim 26899 nvi 28541 nvop 28603 phop 28745 br8d 30516 fgreu 30576 1stpreimas 30605 smatfval 31309 smatrcl 31310 smatlem 31311 fmla0xp 32908 mvhfval 33058 mpst123 33065 br8 33287 frxp3 33400 xpord3pred 33401 nosupbnd2 33552 noinfbnd2 33567 fvtransport 33964 bj-inftyexpitaudisj 34986 rfovcnvf1od 41142 |
Copyright terms: Public domain | W3C validator |