![]() |
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 15121 | . 2 ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ∏cprod 15117 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ral 3086 df-rex 3087 df-rab 3090 df-v 3410 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-xp 5409 df-cnv 5411 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-iota 6149 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-ov 6977 df-oprab 6978 df-mpo 6979 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-seq 13183 df-prod 15118 |
This theorem is referenced by: prodeq12dv 15138 prodeq12rdv 15139 fprodf1o 15158 prodss 15159 fprod1 15175 fprodp1 15181 fprodfac 15185 fprodabs 15186 fprod2d 15193 fprodcom2 15196 risefacval 15220 fallfacval 15221 risefacval2 15222 fallfacval2 15223 risefacp1 15241 fallfacp1 15242 fallfacval4 15255 fprodefsum 15306 prmoval 16223 prmop1 16228 prmgapprmo 16252 gausslemma2dlem4 25662 breprexplema 31581 breprexplemc 31583 breprexp 31584 circlemethhgt 31594 bcprod 32527 dvmptfprodlem 41693 dvmptfprod 41694 ovnval 42288 hoiprodp1 42335 hoidmv1le 42341 hspmbllem1 42373 fmtnorec2 43107 |
Copyright terms: Public domain | W3C validator |