Theorem ixpeq2dv 8934

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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	ixpeq2dva 8933	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Xcixp 8918

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-ss 3916  df-ixp 8919

This theorem is used by:  prdsval  17619  brssc  17982  isfunc  18032  natfval  18117  isnat  18118  dprdval  20212  elpt  23884  elptr  23885  dfac14  23930  ixpeq12dv  36985  hoicvrrex  47535  ovncvrrp  47543  ovnsubaddlem1  47549  ovnsubadd  47551  hoidmvlelem3  47576  hoidmvle  47579  ovnhoilem1  47580  ovnhoilem2  47581  ovnhoi  47582  hspval  47588  ovncvr2  47590  hspmbllem2  47606  hspmbl  47608  hoimbl  47610  opnvonmbl  47613  ovnovollem1  47635  ovnovollem3  47637  iinhoiicclem  47652  iinhoiicc  47653  vonioolem2  47660  vonioo  47661  vonicclem2  47663  vonicc  47664