Theorem ixpeq2dv 8163

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

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  Xcixp 8147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-in 3775  df-ss 3782  df-ixp 8148

This theorem is referenced by:  prdsval  16427  brssc  16785  isfunc  16835  natfval  16917  isnat  16918  dprdval  18715  elpt  21701  elptr  21702  dfac14  21747  hoicvrrex  41505  ovncvrrp  41513  ovnsubaddlem1  41519  ovnsubadd  41521  hoidmvlelem3  41546  hoidmvle  41549  ovnhoilem1  41550  ovnhoilem2  41551  ovnhoi  41552  hspval  41558  ovncvr2  41560  hspmbllem2  41576  hspmbl  41578  hoimbl  41580  opnvonmbl  41583  ovnovollem1  41605  ovnovollem3  41607  iinhoiicclem  41622  iinhoiicc  41623  vonioolem2  41630  vonioo  41631  vonicclem2  41633  vonicc  41634