![]() |
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 8951 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 Xcixp 8936 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-ss 3980 df-ixp 8937 |
This theorem is referenced by: prdsval 17502 brssc 17862 isfunc 17915 natfval 18001 isnat 18002 dprdval 20038 elpt 23596 elptr 23597 dfac14 23642 ixpeq12dv 36199 hoicvrrex 46512 ovncvrrp 46520 ovnsubaddlem1 46526 ovnsubadd 46528 hoidmvlelem3 46553 hoidmvle 46556 ovnhoilem1 46557 ovnhoilem2 46558 ovnhoi 46559 hspval 46565 ovncvr2 46567 hspmbllem2 46583 hspmbl 46585 hoimbl 46587 opnvonmbl 46590 ovnovollem1 46612 ovnovollem3 46614 iinhoiicclem 46629 iinhoiicc 46630 vonioolem2 46637 vonioo 46638 vonicclem2 46640 vonicc 46641 |
Copyright terms: Public domain | W3C validator |