| 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 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
| 3 | 2 | ixpeq2dva 8952 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 Xcixp 8937 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-ss 3968 df-ixp 8938 |
| This theorem is referenced by: prdsval 17500 brssc 17858 isfunc 17909 natfval 17994 isnat 17995 dprdval 20023 elpt 23580 elptr 23581 dfac14 23626 ixpeq12dv 36217 hoicvrrex 46571 ovncvrrp 46579 ovnsubaddlem1 46585 ovnsubadd 46587 hoidmvlelem3 46612 hoidmvle 46615 ovnhoilem1 46616 ovnhoilem2 46617 ovnhoi 46618 hspval 46624 ovncvr2 46626 hspmbllem2 46642 hspmbl 46644 hoimbl 46646 opnvonmbl 46649 ovnovollem1 46671 ovnovollem3 46673 iinhoiicclem 46688 iinhoiicc 46689 vonioolem2 46696 vonioo 46697 vonicclem2 46699 vonicc 46700 |
| Copyright terms: Public domain | W3C validator |