Theorem ixpeq2dv 8886

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Xcixp 8870

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-ss 3931  df-ixp 8871

This theorem is referenced by:  prdsval  17418  brssc  17776  isfunc  17826  natfval  17911  isnat  17912  dprdval  19935  elpt  23459  elptr  23460  dfac14  23505  ixpeq12dv  36204  hoicvrrex  46554  ovncvrrp  46562  ovnsubaddlem1  46568  ovnsubadd  46570  hoidmvlelem3  46595  hoidmvle  46598  ovnhoilem1  46599  ovnhoilem2  46600  ovnhoi  46601  hspval  46607  ovncvr2  46609  hspmbllem2  46625  hspmbl  46627  hoimbl  46629  opnvonmbl  46632  ovnovollem1  46654  ovnovollem3  46656  iinhoiicclem  46671  iinhoiicc  46672  vonioolem2  46679  vonioo  46680  vonicclem2  46682  vonicc  46683