Theorem ixpeq2dv 8910

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Xcixp 8894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-ss 3930  df-ixp 8895

This theorem is referenced by:  prdsval  17507  brssc  17870  isfunc  17920  natfval  18005  isnat  18006  dprdval  20074  elpt  23697  elptr  23698  dfac14  23743  ixpeq12dv  36616  hoicvrrex  47161  ovncvrrp  47169  ovnsubaddlem1  47175  ovnsubadd  47177  hoidmvlelem3  47202  hoidmvle  47205  ovnhoilem1  47206  ovnhoilem2  47207  ovnhoi  47208  hspval  47214  ovncvr2  47216  hspmbllem2  47232  hspmbl  47234  hoimbl  47236  opnvonmbl  47239  ovnovollem1  47261  ovnovollem3  47263  iinhoiicclem  47278  iinhoiicc  47279  vonioolem2  47286  vonioo  47287  vonicclem2  47289  vonicc  47290