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 483 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | ixpeq2dva 8470 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2110 Xcixp 8455 |
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 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-in 3942 df-ss 3951 df-ixp 8456 |
This theorem is referenced by: prdsval 16722 brssc 17078 isfunc 17128 natfval 17210 isnat 17211 dprdval 19119 elpt 22174 elptr 22175 dfac14 22220 hoicvrrex 42832 ovncvrrp 42840 ovnsubaddlem1 42846 ovnsubadd 42848 hoidmvlelem3 42873 hoidmvle 42876 ovnhoilem1 42877 ovnhoilem2 42878 ovnhoi 42879 hspval 42885 ovncvr2 42887 hspmbllem2 42903 hspmbl 42905 hoimbl 42907 opnvonmbl 42910 ovnovollem1 42932 ovnovollem3 42934 iinhoiicclem 42949 iinhoiicc 42950 vonioolem2 42957 vonioo 42958 vonicclem2 42960 vonicc 42961 |
Copyright terms: Public domain | W3C validator |