Theorem ixpeq2dv 8907

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Xcixp 8891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-ss 3922  df-ixp 8892

This theorem is referenced by:  prdsval  17503  brssc  17866  isfunc  17916  natfval  18001  isnat  18002  dprdval  20070  elpt  23729  elptr  23730  dfac14  23775  ixpeq12dv  36728  hoicvrrex  47270  ovncvrrp  47278  ovnsubaddlem1  47284  ovnsubadd  47286  hoidmvlelem3  47311  hoidmvle  47314  ovnhoilem1  47315  ovnhoilem2  47316  ovnhoi  47317  hspval  47323  ovncvr2  47325  hspmbllem2  47341  hspmbl  47343  hoimbl  47345  opnvonmbl  47348  ovnovollem1  47370  ovnovollem3  47372  iinhoiicclem  47387  iinhoiicc  47388  vonioolem2  47395  vonioo  47396  vonicclem2  47398  vonicc  47399