Theorem ixpeq2dv 8659

Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)

Hypothesis

Ref	Expression
ixpeq2dv.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
ixpeq2dv	⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem ixpeq2dv

Step	Hyp	Ref	Expression
1		ixpeq2dv.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	ixpeq2dva 8658	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  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:  prdsval  17083  brssc  17443  isfunc  17495  natfval  17578  isnat  17579  dprdval  19521  elpt  22631  elptr  22632  dfac14  22677  hoicvrrex  43984  ovncvrrp  43992  ovnsubaddlem1  43998  ovnsubadd  44000  hoidmvlelem3  44025  hoidmvle  44028  ovnhoilem1  44029  ovnhoilem2  44030  ovnhoi  44031  hspval  44037  ovncvr2  44039  hspmbllem2  44055  hspmbl  44057  hoimbl  44059  opnvonmbl  44062  ovnovollem1  44084  ovnovollem3  44086  iinhoiicclem  44101  iinhoiicc  44102  vonioolem2  44109  vonioo  44110  vonicclem2  44112  vonicc  44113