Theorem ixpeq2dv 8917

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-ss 3923  df-ixp 8902

This theorem is used by:  prdsval  17530  brssc  17893  isfunc  17943  natfval  18028  isnat  18029  dprdval  20119  elpt  23780  elptr  23781  dfac14  23826  ixpeq12dv  36785  hoicvrrex  47328  ovncvrrp  47336  ovnsubaddlem1  47342  ovnsubadd  47344  hoidmvlelem3  47369  hoidmvle  47372  ovnhoilem1  47373  ovnhoilem2  47374  ovnhoi  47375  hspval  47381  ovncvr2  47383  hspmbllem2  47399  hspmbl  47401  hoimbl  47403  opnvonmbl  47406  ovnovollem1  47428  ovnovollem3  47430  iinhoiicclem  47445  iinhoiicc  47446  vonioolem2  47453  vonioo  47454  vonicclem2  47456  vonicc  47457