Theorem ixpeq2dv 8471

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  Xcixp 8455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-in 3942  df-ss 3951  df-ixp 8456

This theorem is referenced by:  prdsval  16722  brssc  17078  isfunc  17128  natfval  17210  isnat  17211  dprdval  19119  elpt  22174  elptr  22175  dfac14  22220  hoicvrrex  42832  ovncvrrp  42840  ovnsubaddlem1  42846  ovnsubadd  42848  hoidmvlelem3  42873  hoidmvle  42876  ovnhoilem1  42877  ovnhoilem2  42878  ovnhoi  42879  hspval  42885  ovncvr2  42887  hspmbllem2  42903  hspmbl  42905  hoimbl  42907  opnvonmbl  42910  ovnovollem1  42932  ovnovollem3  42934  iinhoiicclem  42949  iinhoiicc  42950  vonioolem2  42957  vonioo  42958  vonicclem2  42960  vonicc  42961