Theorem ixpeq2dva 8459

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Xcixp 8444

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-ixp 8445

This theorem is referenced by:  ixpeq2dv  8460  dfac9  9547  xpsrnbas  16836  funcpropd  17162  natpropd  17238  prdsmgp  19356  frlmip  20467  elptr2  22179  dfac14  22223  xkoptsub  22259  prdsxmslem2  23136  rrxip  23994  ptrest  35056  prdsbnd2  35233  hoidmvlelem3  43236  ovnhoilem1  43240  ovnhoilem2  43241  hoicoto2  43244  ovnlecvr2  43249  ovncvr2  43250  ovnovollem1  43295  ovnovollem2  43296  hoimbl2  43304  vonhoire  43311  iccvonmbllem  43317  vonioolem2  43320  vonicclem2  43323  vonn0ioo2  43329  vonn0icc2  43331