Theorem ixpeq2dv 8889

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Xcixp 8873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-ss 3934  df-ixp 8874

This theorem is referenced by:  prdsval  17425  brssc  17783  isfunc  17833  natfval  17918  isnat  17919  dprdval  19942  elpt  23466  elptr  23467  dfac14  23512  ixpeq12dv  36211  hoicvrrex  46561  ovncvrrp  46569  ovnsubaddlem1  46575  ovnsubadd  46577  hoidmvlelem3  46602  hoidmvle  46605  ovnhoilem1  46606  ovnhoilem2  46607  ovnhoi  46608  hspval  46614  ovncvr2  46616  hspmbllem2  46632  hspmbl  46634  hoimbl  46636  opnvonmbl  46639  ovnovollem1  46661  ovnovollem3  46663  iinhoiicclem  46678  iinhoiicc  46679  vonioolem2  46686  vonioo  46687  vonicclem2  46689  vonicc  46690