Theorem ixpeq2dv 8701

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  Xcixp 8685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-ixp 8686

This theorem is referenced by:  prdsval  17166  brssc  17526  isfunc  17579  natfval  17662  isnat  17663  dprdval  19606  elpt  22723  elptr  22724  dfac14  22769  hoicvrrex  44094  ovncvrrp  44102  ovnsubaddlem1  44108  ovnsubadd  44110  hoidmvlelem3  44135  hoidmvle  44138  ovnhoilem1  44139  ovnhoilem2  44140  ovnhoi  44141  hspval  44147  ovncvr2  44149  hspmbllem2  44165  hspmbl  44167  hoimbl  44169  opnvonmbl  44172  ovnovollem1  44194  ovnovollem3  44196  iinhoiicclem  44211  iinhoiicc  44212  vonioolem2  44219  vonioo  44220  vonicclem2  44222  vonicc  44223