![]() |
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 14845 | . 2 ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1630 ∏cprod 14841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-rab 3069 df-v 3351 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 df-uni 4573 df-br 4785 df-opab 4845 df-mpt 4862 df-xp 5255 df-cnv 5257 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-iota 5994 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-ov 6795 df-oprab 6796 df-mpt2 6797 df-wrecs 7558 df-recs 7620 df-rdg 7658 df-seq 13008 df-prod 14842 |
This theorem is referenced by: prodeq12dv 14862 prodeq12rdv 14863 fprodf1o 14882 prodss 14883 fprod1 14899 fprodp1 14905 fprodfac 14909 fprodabs 14910 fprod2d 14917 fprodcom2 14920 risefacval 14944 fallfacval 14945 risefacval2 14946 fallfacval2 14947 risefacp1 14965 fallfacp1 14966 fallfacval4 14979 fprodefsum 15030 prmoval 15943 prmop1 15948 prmgapprmo 15972 gausslemma2dlem4 25314 breprexplema 31042 breprexplemc 31044 breprexp 31045 circlemethhgt 31055 bcprod 31956 dvmptfprodlem 40671 dvmptfprod 40672 ovnval 41269 hoiprodp1 41316 hoidmv1le 41322 hspmbllem1 41354 fmtnorec2 41973 |
Copyright terms: Public domain | W3C validator |