![]() |
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 473 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | ixpeq2dva 8162 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 Xcixp 8147 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ral 3093 df-in 3775 df-ss 3782 df-ixp 8148 |
This theorem is referenced by: prdsval 16427 brssc 16785 isfunc 16835 natfval 16917 isnat 16918 dprdval 18715 elpt 21701 elptr 21702 dfac14 21747 hoicvrrex 41505 ovncvrrp 41513 ovnsubaddlem1 41519 ovnsubadd 41521 hoidmvlelem3 41546 hoidmvle 41549 ovnhoilem1 41550 ovnhoilem2 41551 ovnhoi 41552 hspval 41558 ovncvr2 41560 hspmbllem2 41576 hspmbl 41578 hoimbl 41580 opnvonmbl 41583 ovnovollem1 41605 ovnovollem3 41607 iinhoiicclem 41622 iinhoiicc 41623 vonioolem2 41630 vonioo 41631 vonicclem2 41633 vonicc 41634 |
Copyright terms: Public domain | W3C validator |