![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ixpeq2dv | Structured version Visualization version GIF version |
Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
Ref | Expression |
---|---|
ixpeq2dv.1 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
ixpeq2dv | ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ixpeq2dv.1 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐶) | |
2 | 1 | adantr 472 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | ixpeq2dva 8077 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1620 ∈ wcel 2127 Xcixp 8062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ral 3043 df-in 3710 df-ss 3717 df-ixp 8063 |
This theorem is referenced by: prdsval 16288 brssc 16646 isfunc 16696 natfval 16778 isnat 16779 dprdval 18573 elpt 21548 elptr 21549 dfac14 21594 hoicvrrex 41245 ovncvrrp 41253 ovnsubaddlem1 41259 ovnsubadd 41261 hoidmvlelem3 41286 hoidmvle 41289 ovnhoilem1 41290 ovnhoilem2 41291 ovnhoi 41292 hspval 41298 ovncvr2 41300 hspmbllem2 41316 hspmbl 41318 hoimbl 41320 opnvonmbl 41323 ovnovollem1 41345 ovnovollem3 41347 iinhoiicclem 41362 iinhoiicc 41363 vonioolem2 41370 vonioo 41371 vonicclem2 41373 vonicc 41374 |
Copyright terms: Public domain | W3C validator |