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 4796 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 〈cop 4566 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 |
This theorem is referenced by: oteq1 4805 oteq2 4806 opth 5360 elsnxp 6136 cbvoprab2 7236 fvproj 7822 unxpdomlem1 8716 djulf1o 9335 djurf1o 9336 mulcanenq 10376 ax1rid 10577 axrnegex 10578 fseq1m1p1 12976 uzrdglem 13319 pfxswrd 14062 swrdccat 14091 swrdccat3blem 14095 cshw0 14150 cshwmodn 14151 s2prop 14263 s4prop 14266 fsum2dlem 15119 fprod2dlem 15328 ruclem1 15578 imasaddvallem 16796 iscatd2 16946 moni 17000 homadmcd 17296 curf1 17469 curf1cl 17472 curf2 17473 hofcl 17503 gsum2dlem2 19085 imasdsf1olem 22977 ovoliunlem1 24097 cxpcn3 25323 axlowdimlem15 26736 axlowdim 26741 nvi 28385 nvop 28447 phop 28589 br8d 30355 fgreu 30411 1stpreimas 30435 smatfval 31055 smatrcl 31056 smatlem 31057 fmla0xp 32625 mvhfval 32775 mpst123 32782 br8 32987 nosupbnd2 33211 fvtransport 33488 bj-inftyexpitaudisj 34481 rfovcnvf1od 40343 |
Copyright terms: Public domain | W3C validator |