Theorem ixpeq2dva 8909

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 3163	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		ixpeq2 8908	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 18	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  Xcixp 8894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-ss 3930  df-ixp 8895

This theorem is referenced by:  ixpeq2dv  8910  dfac9  10119  xpsrnbas  17624  funcpropd  17958  natpropd  18035  prdsmgp  20226  frlmip  21896  elptr2  23699  dfac14  23743  xkoptsub  23779  prdsxmslem2  24654  rrxip  25517  ptrest  38157  prdsbnd2  38333  hoidmvlelem3  47202  ovnhoilem1  47206  ovnhoilem2  47207  hoicoto2  47210  ovnlecvr2  47215  ovncvr2  47216  ovnovollem1  47261  ovnovollem2  47262  hoimbl2  47270  vonhoire  47277  iccvonmbllem  47283  vonioolem2  47286  vonicclem2  47289  vonn0ioo2  47295  vonn0icc2  47297