Theorem ixpeq2dva 8913

Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)

Hypothesis

Ref	Expression
ixpeq2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
ixpeq2dva	⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem ixpeq2dva

Step	Hyp	Ref	Expression
1		ixpeq2dva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3164	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		ixpeq2 8912	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 18	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2150  ∀wral 3086  Xcixp 8898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ral 3087  df-ss 3930  df-ixp 8899

This theorem is referenced by:  ixpeq2dv  8914  dfac9  10123  xpsrnbas  17628  funcpropd  17962  natpropd  18039  prdsmgp  20230  frlmip  21911  elptr2  23714  dfac14  23758  xkoptsub  23794  prdsxmslem2  24669  rrxip  25532  ptrest  38218  prdsbnd2  38394  hoidmvlelem3  47263  ovnhoilem1  47267  ovnhoilem2  47268  hoicoto2  47271  ovnlecvr2  47276  ovncvr2  47277  ovnovollem1  47322  ovnovollem2  47323  hoimbl2  47331  vonhoire  47338  iccvonmbllem  47344  vonioolem2  47347  vonicclem2  47350  vonn0ioo2  47356  vonn0icc2  47358