![]() |
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 481 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | ixpeq2dva 8332 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1525 ∈ wcel 2083 Xcixp 8317 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-in 3872 df-ss 3880 df-ixp 8318 |
This theorem is referenced by: prdsval 16561 brssc 16917 isfunc 16967 natfval 17049 isnat 17050 dprdval 18846 elpt 21868 elptr 21869 dfac14 21914 hoicvrrex 42402 ovncvrrp 42410 ovnsubaddlem1 42416 ovnsubadd 42418 hoidmvlelem3 42443 hoidmvle 42446 ovnhoilem1 42447 ovnhoilem2 42448 ovnhoi 42449 hspval 42455 ovncvr2 42457 hspmbllem2 42473 hspmbl 42475 hoimbl 42477 opnvonmbl 42480 ovnovollem1 42502 ovnovollem3 42504 iinhoiicclem 42519 iinhoiicc 42520 vonioolem2 42527 vonioo 42528 vonicclem2 42530 vonicc 42531 |
Copyright terms: Public domain | W3C validator |