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 3182 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
3 | ixpeq2 8475 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ∀wral 3138 Xcixp 8461 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-in 3943 df-ss 3952 df-ixp 8462 |
This theorem is referenced by: ixpeq2dv 8477 dfac9 9562 xpsrnbas 16844 funcpropd 17170 natpropd 17246 prdsmgp 19360 frlmip 20922 elptr2 22182 dfac14 22226 xkoptsub 22262 prdsxmslem2 23139 rrxip 23993 ptrest 34906 prdsbnd2 35088 hoidmvlelem3 42899 ovnhoilem1 42903 ovnhoilem2 42904 hoicoto2 42907 ovnlecvr2 42912 ovncvr2 42913 ovnovollem1 42958 ovnovollem2 42959 hoimbl2 42967 vonhoire 42974 iccvonmbllem 42980 vonioolem2 42983 vonicclem2 42986 vonn0ioo2 42992 vonn0icc2 42994 |
Copyright terms: Public domain | W3C validator |