Theorem ixpeq2dv 8500

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Xcixp 8484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-v 3411  df-in 3867  df-ss 3877  df-ixp 8485

This theorem is referenced by:  prdsval  16791  brssc  17148  isfunc  17198  natfval  17280  isnat  17281  dprdval  19198  elpt  22277  elptr  22278  dfac14  22323  hoicvrrex  43589  ovncvrrp  43597  ovnsubaddlem1  43603  ovnsubadd  43605  hoidmvlelem3  43630  hoidmvle  43633  ovnhoilem1  43634  ovnhoilem2  43635  ovnhoi  43636  hspval  43642  ovncvr2  43644  hspmbllem2  43660  hspmbl  43662  hoimbl  43664  opnvonmbl  43667  ovnovollem1  43689  ovnovollem3  43691  iinhoiicclem  43706  iinhoiicc  43707  vonioolem2  43714  vonioo  43715  vonicclem2  43717  vonicc  43718