Theorem ixpeq2dv 8851

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 8850	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Xcixp 8835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-ss 3918  df-ixp 8836

This theorem is referenced by:  prdsval  17375  brssc  17738  isfunc  17788  natfval  17873  isnat  17874  dprdval  19934  elpt  23516  elptr  23517  dfac14  23562  ixpeq12dv  36410  hoicvrrex  46810  ovncvrrp  46818  ovnsubaddlem1  46824  ovnsubadd  46826  hoidmvlelem3  46851  hoidmvle  46854  ovnhoilem1  46855  ovnhoilem2  46856  ovnhoi  46857  hspval  46863  ovncvr2  46865  hspmbllem2  46881  hspmbl  46883  hoimbl  46885  opnvonmbl  46888  ovnovollem1  46910  ovnovollem3  46912  iinhoiicclem  46927  iinhoiicc  46928  vonioolem2  46935  vonioo  46936  vonicclem2  46938  vonicc  46939