Theorem ixpeq2dv 8849

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Xcixp 8833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-ss 3916  df-ixp 8834

This theorem is referenced by:  prdsval  17373  brssc  17736  isfunc  17786  natfval  17871  isnat  17872  dprdval  19932  elpt  23514  elptr  23515  dfac14  23560  ixpeq12dv  36359  hoicvrrex  46742  ovncvrrp  46750  ovnsubaddlem1  46756  ovnsubadd  46758  hoidmvlelem3  46783  hoidmvle  46786  ovnhoilem1  46787  ovnhoilem2  46788  ovnhoi  46789  hspval  46795  ovncvr2  46797  hspmbllem2  46813  hspmbl  46815  hoimbl  46817  opnvonmbl  46820  ovnovollem1  46842  ovnovollem3  46844  iinhoiicclem  46859  iinhoiicc  46860  vonioolem2  46867  vonioo  46868  vonicclem2  46870  vonicc  46871