Theorem ixpeq2dv 8948

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Xcixp 8932

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-ss 3897  df-ixp 8933

This theorem is used by:  prdsval  17635  brssc  17998  isfunc  18048  natfval  18133  isnat  18134  dprdval  20228  elpt  23900  elptr  23901  dfac14  23946  ixpeq12dv  37101  hoicvrrex  47674  ovncvrrp  47682  ovnsubaddlem1  47688  ovnsubadd  47690  hoidmvlelem3  47715  hoidmvle  47718  ovnhoilem1  47719  ovnhoilem2  47720  ovnhoi  47721  hspval  47727  ovncvr2  47729  hspmbllem2  47745  hspmbl  47747  hoimbl  47749  opnvonmbl  47752  ovnovollem1  47774  ovnovollem3  47776  iinhoiicclem  47791  iinhoiicc  47792  vonioolem2  47799  vonioo  47800  vonicclem2  47802  vonicc  47803