Theorem ixpeq2dv 8863

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

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

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 3928  df-ixp 8848

This theorem is referenced by:  prdsval  17394  brssc  17756  isfunc  17806  natfval  17891  isnat  17892  dprdval  19919  elpt  23492  elptr  23493  dfac14  23538  ixpeq12dv  36197  hoicvrrex  46547  ovncvrrp  46555  ovnsubaddlem1  46561  ovnsubadd  46563  hoidmvlelem3  46588  hoidmvle  46591  ovnhoilem1  46592  ovnhoilem2  46593  ovnhoi  46594  hspval  46600  ovncvr2  46602  hspmbllem2  46618  hspmbl  46620  hoimbl  46622  opnvonmbl  46625  ovnovollem1  46647  ovnovollem3  46649  iinhoiicclem  46664  iinhoiicc  46665  vonioolem2  46672  vonioo  46673  vonicclem2  46675  vonicc  46676