Theorem ixpeq2dv 8927

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Xcixp 8911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-ss 3943  df-ixp 8912

This theorem is referenced by:  prdsval  17469  brssc  17827  isfunc  17877  natfval  17962  isnat  17963  dprdval  19986  elpt  23510  elptr  23511  dfac14  23556  ixpeq12dv  36234  hoicvrrex  46585  ovncvrrp  46593  ovnsubaddlem1  46599  ovnsubadd  46601  hoidmvlelem3  46626  hoidmvle  46629  ovnhoilem1  46630  ovnhoilem2  46631  ovnhoi  46632  hspval  46638  ovncvr2  46640  hspmbllem2  46656  hspmbl  46658  hoimbl  46660  opnvonmbl  46663  ovnovollem1  46685  ovnovollem3  46687  iinhoiicclem  46702  iinhoiicc  46703  vonioolem2  46710  vonioo  46711  vonicclem2  46713  vonicc  46714