Theorem ixpeq2dv 8920

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-ss 3916  df-ixp 8905

This theorem is used by:  prdsval  17540  brssc  17903  isfunc  17953  natfval  18038  isnat  18039  dprdval  20132  elpt  23798  elptr  23799  dfac14  23844  ixpeq12dv  36836  hoicvrrex  47384  ovncvrrp  47392  ovnsubaddlem1  47398  ovnsubadd  47400  hoidmvlelem3  47425  hoidmvle  47428  ovnhoilem1  47429  ovnhoilem2  47430  ovnhoi  47431  hspval  47437  ovncvr2  47439  hspmbllem2  47455  hspmbl  47457  hoimbl  47459  opnvonmbl  47462  ovnovollem1  47484  ovnovollem3  47486  iinhoiicclem  47501  iinhoiicc  47502  vonioolem2  47509  vonioo  47510  vonicclem2  47512  vonicc  47513