Theorem ixpeq2dv 8971

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Xcixp 8955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-ss 3993  df-ixp 8956

This theorem is referenced by:  prdsval  17515  brssc  17875  isfunc  17928  natfval  18014  isnat  18015  dprdval  20047  elpt  23601  elptr  23602  dfac14  23647  ixpeq12dv  36182  hoicvrrex  46477  ovncvrrp  46485  ovnsubaddlem1  46491  ovnsubadd  46493  hoidmvlelem3  46518  hoidmvle  46521  ovnhoilem1  46522  ovnhoilem2  46523  ovnhoi  46524  hspval  46530  ovncvr2  46532  hspmbllem2  46548  hspmbl  46550  hoimbl  46552  opnvonmbl  46555  ovnovollem1  46577  ovnovollem3  46579  iinhoiicclem  46594  iinhoiicc  46595  vonioolem2  46602  vonioo  46603  vonicclem2  46605  vonicc  46606