Theorem ixpeq2dv 8840

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-ss 3920  df-ixp 8825

This theorem is referenced by:  prdsval  17359  brssc  17721  isfunc  17771  natfval  17856  isnat  17857  dprdval  19884  elpt  23457  elptr  23458  dfac14  23503  ixpeq12dv  36190  hoicvrrex  46537  ovncvrrp  46545  ovnsubaddlem1  46551  ovnsubadd  46553  hoidmvlelem3  46578  hoidmvle  46581  ovnhoilem1  46582  ovnhoilem2  46583  ovnhoi  46584  hspval  46590  ovncvr2  46592  hspmbllem2  46608  hspmbl  46610  hoimbl  46612  opnvonmbl  46615  ovnovollem1  46637  ovnovollem3  46639  iinhoiicclem  46654  iinhoiicc  46655  vonioolem2  46662  vonioo  46663  vonicclem2  46665  vonicc  46666