Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ixpeq2dva | Structured version Visualization version GIF version |
Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
Ref | Expression |
---|---|
ixpeq2dva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
ixpeq2dva | ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ixpeq2dva.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) | |
2 | 1 | ralrimiva 2949 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
3 | ixpeq2 7808 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Xcixp 7794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-in 3547 df-ss 3554 df-ixp 7795 |
This theorem is referenced by: ixpeq2dv 7810 dfac9 8841 xpsfrn2 16053 xpslem 16056 funcpropd 16383 natpropd 16459 prdsmgp 18433 frlmip 19936 elptr2 21187 dfac14 21231 xkoptsub 21267 prdsxmslem2 22144 rrxip 22986 ptrest 32578 prdsbnd2 32764 hoidmvlelem3 39487 ovnhoilem1 39491 ovnhoilem2 39492 hoicoto2 39495 ovnlecvr2 39500 ovncvr2 39501 ovnovollem1 39546 ovnovollem2 39547 hoimbl2 39555 vonhoire 39563 iccvonmbllem 39569 vonioolem2 39572 vonicclem2 39575 vonn0ioo2 39581 vonn0icc2 39583 |
Copyright terms: Public domain | W3C validator |