Theorem ixpeq2dva 8902

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  Xcixp 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3954  df-ss 3964  df-ixp 8888

This theorem is referenced by:  ixpeq2dv  8903  dfac9  10127  xpsrnbas  17513  funcpropd  17847  natpropd  17925  prdsmgp  20125  frlmip  21324  elptr2  23069  dfac14  23113  xkoptsub  23149  prdsxmslem2  24029  rrxip  24898  ptrest  36475  prdsbnd2  36651  hoidmvlelem3  45299  ovnhoilem1  45303  ovnhoilem2  45304  hoicoto2  45307  ovnlecvr2  45312  ovncvr2  45313  ovnovollem1  45358  ovnovollem2  45359  hoimbl2  45367  vonhoire  45374  iccvonmbllem  45380  vonioolem2  45383  vonicclem2  45386  vonn0ioo2  45392  vonn0icc2  45394