| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > prodeq1d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
| Ref | Expression |
|---|---|
| prodeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| prodeq1d | ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prodeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | prodeq1 15949 | . 2 ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1563 ∏cprod 15945 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-mpt 5186 df-xp 5657 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-iota 6481 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-seq 14026 df-prod 15946 |
| This theorem is referenced by: prodeq12dv 15968 prodeq12rdv 15969 fprodf1o 15988 prodss 15989 fprod1 16005 fprodp1 16011 fprodfac 16015 fprodabs 16016 fprod2d 16023 fprodcom2 16026 risefacval 16050 fallfacval 16051 risefacval2 16052 fallfacval2 16053 risefacp1 16071 fallfacp1 16072 fallfacval4 16085 fprodefsum 16137 prmoval 17081 prmop1 17086 prmgapprmo 17110 gausslemma2dlem4 27487 breprexplema 34929 breprexplemc 34931 breprexp 34932 circlemethhgt 34942 bcprod 36096 aks4d1p1 42700 dvmptfprodlem 46517 dvmptfprod 46518 ovnval 47114 hoiprodp1 47161 hoidmv1le 47167 hspmbllem1 47199 fmtnorec2 48151 |
| Copyright terms: Public domain | W3C validator |