Theorem ixpeq2dv 8851

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Xcixp 8835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-ss 3900  df-ixp 8836

This theorem is referenced by:  prdsval  17409  brssc  17772  isfunc  17822  natfval  17907  isnat  17908  dprdval  19971  elpt  23555  elptr  23556  dfac14  23601  ixpeq12dv  36444  hoicvrrex  46999  ovncvrrp  47007  ovnsubaddlem1  47013  ovnsubadd  47015  hoidmvlelem3  47040  hoidmvle  47043  ovnhoilem1  47044  ovnhoilem2  47045  ovnhoi  47046  hspval  47052  ovncvr2  47054  hspmbllem2  47070  hspmbl  47072  hoimbl  47074  opnvonmbl  47077  ovnovollem1  47099  ovnovollem3  47101  iinhoiicclem  47116  iinhoiicc  47117  vonioolem2  47124  vonioo  47125  vonicclem2  47127  vonicc  47128