Theorem ixpeq2dva 8970

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  Xcixp 8955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-ss 3993  df-ixp 8956

This theorem is referenced by:  ixpeq2dv  8971  dfac9  10206  xpsrnbas  17631  funcpropd  17967  natpropd  18046  prdsmgp  20178  frlmip  21821  elptr2  23603  dfac14  23647  xkoptsub  23683  prdsxmslem2  24563  rrxip  25443  ptrest  37579  prdsbnd2  37755  hoidmvlelem3  46518  ovnhoilem1  46522  ovnhoilem2  46523  hoicoto2  46526  ovnlecvr2  46531  ovncvr2  46532  ovnovollem1  46577  ovnovollem2  46578  hoimbl2  46586  vonhoire  46593  iccvonmbllem  46599  vonioolem2  46602  vonicclem2  46605  vonn0ioo2  46611  vonn0icc2  46613