Theorem ixpeq2dv 8895

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  Xcixp 8879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-ss 3921  df-ixp 8880

This theorem is referenced by:  prdsval  17484  brssc  17847  isfunc  17897  natfval  17982  isnat  17983  dprdval  20045  elpt  23629  elptr  23630  dfac14  23675  ixpeq12dv  36573  hoicvrrex  47127  ovncvrrp  47135  ovnsubaddlem1  47141  ovnsubadd  47143  hoidmvlelem3  47168  hoidmvle  47171  ovnhoilem1  47172  ovnhoilem2  47173  ovnhoi  47174  hspval  47180  ovncvr2  47182  hspmbllem2  47198  hspmbl  47200  hoimbl  47202  opnvonmbl  47205  ovnovollem1  47227  ovnovollem3  47229  iinhoiicclem  47244  iinhoiicc  47245  vonioolem2  47252  vonioo  47253  vonicclem2  47255  vonicc  47256