| 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 4873 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 〈cop 4632 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 |
| This theorem is referenced by: oteq1 4882 oteq2 4883 opth 5481 elsnxp 6311 cbvoprab2 7521 cbvoprab12v 7523 fvproj 8159 unxpdomlem1 9286 djulf1o 9952 djurf1o 9953 mulcanenq 11000 ax1rid 11201 axrnegex 11202 fseq1m1p1 13639 uzrdglem 13998 pfxswrd 14744 swrdccat 14773 swrdccat3blem 14777 cshw0 14832 cshwmodn 14833 s2prop 14946 s4prop 14949 fsum2dlem 15806 fprod2dlem 16016 ruclem1 16267 imasaddvallem 17574 iscatd2 17724 moni 17780 homadmcd 18087 curf1 18270 curf1cl 18273 curf2 18274 hofcl 18304 gsum2dlem2 19989 pzriprnglem10 21501 imasdsf1olem 24383 ovoliunlem1 25537 cxpcn3 26791 nosupbnd2 27761 noinfbnd2 27776 noseqrdglem 28311 axlowdimlem15 28971 axlowdim 28976 nvi 30633 nvop 30695 phop 30837 br8d 32622 fgreu 32682 1stpreimas 32715 rlocval 33263 rloccring 33274 smatfval 33794 smatrcl 33795 smatlem 33796 fmla0xp 35388 mvhfval 35538 mpst123 35545 br8 35756 fvtransport 36033 cbvoprab1vw 36238 cbvoprab2vw 36239 cbvoprab1davw 36272 cbvoprab2davw 36273 cbvoprab12davw 36276 bj-inftyexpitaudisj 37206 rfovcnvf1od 44017 tposcurf2val 49001 oppcthinendcALT 49090 |
| Copyright terms: Public domain | W3C validator |