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  46800  ovncvrrp  46808  ovnsubaddlem1  46814  ovnsubadd  46816  hoidmvlelem3  46841  hoidmvle  46844  ovnhoilem1  46845  ovnhoilem2  46846  ovnhoi  46847  hspval  46853  ovncvr2  46855  hspmbllem2  46871  hspmbl  46873  hoimbl  46875  opnvonmbl  46878  ovnovollem1  46900  ovnovollem3  46902  iinhoiicclem  46917  iinhoiicc  46918  vonioolem2  46925  vonioo  46926  vonicclem2  46928  vonicc  46929