Theorem ixpeq2dva 8658

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  Xcixp 8643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-ixp 8644

This theorem is referenced by:  ixpeq2dv  8659  dfac9  9823  xpsrnbas  17199  funcpropd  17532  natpropd  17610  prdsmgp  19764  frlmip  20895  elptr2  22633  dfac14  22677  xkoptsub  22713  prdsxmslem2  23591  rrxip  24459  ptrest  35703  prdsbnd2  35880  hoidmvlelem3  44025  ovnhoilem1  44029  ovnhoilem2  44030  hoicoto2  44033  ovnlecvr2  44038  ovncvr2  44039  ovnovollem1  44084  ovnovollem2  44085  hoimbl2  44093  vonhoire  44100  iccvonmbllem  44106  vonioolem2  44109  vonicclem2  44112  vonn0ioo2  44118  vonn0icc2  44120