Theorem ixpeq2dva 8831

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2110  ∀wral 3045  Xcixp 8816

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-ss 3917  df-ixp 8817

This theorem is referenced by:  ixpeq2dv  8832  dfac9  10020  xpsrnbas  17467  funcpropd  17801  natpropd  17878  prdsmgp  20062  frlmip  21708  elptr2  23482  dfac14  23526  xkoptsub  23562  prdsxmslem2  24437  rrxip  25310  ptrest  37638  prdsbnd2  37814  hoidmvlelem3  46614  ovnhoilem1  46618  ovnhoilem2  46619  hoicoto2  46622  ovnlecvr2  46627  ovncvr2  46628  ovnovollem1  46673  ovnovollem2  46674  hoimbl2  46682  vonhoire  46689  iccvonmbllem  46695  vonioolem2  46698  vonicclem2  46701  vonn0ioo2  46707  vonn0icc2  46709