Theorem ixpeq2dv 8863

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

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

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 3928  df-ixp 8848

This theorem is referenced by:  prdsval  17394  brssc  17752  isfunc  17802  natfval  17887  isnat  17888  dprdval  19911  elpt  23435  elptr  23436  dfac14  23481  ixpeq12dv  36177  hoicvrrex  46527  ovncvrrp  46535  ovnsubaddlem1  46541  ovnsubadd  46543  hoidmvlelem3  46568  hoidmvle  46571  ovnhoilem1  46572  ovnhoilem2  46573  ovnhoi  46574  hspval  46580  ovncvr2  46582  hspmbllem2  46598  hspmbl  46600  hoimbl  46602  opnvonmbl  46605  ovnovollem1  46627  ovnovollem3  46629  iinhoiicclem  46644  iinhoiicc  46645  vonioolem2  46652  vonioo  46653  vonicclem2  46655  vonicc  46656