Theorem ixpeq2dv 8855

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Xcixp 8839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-ss 3907  df-ixp 8840

This theorem is referenced by:  prdsval  17412  brssc  17775  isfunc  17825  natfval  17910  isnat  17911  dprdval  19974  elpt  23550  elptr  23551  dfac14  23596  ixpeq12dv  36417  hoicvrrex  47005  ovncvrrp  47013  ovnsubaddlem1  47019  ovnsubadd  47021  hoidmvlelem3  47046  hoidmvle  47049  ovnhoilem1  47050  ovnhoilem2  47051  ovnhoi  47052  hspval  47058  ovncvr2  47060  hspmbllem2  47076  hspmbl  47078  hoimbl  47080  opnvonmbl  47083  ovnovollem1  47105  ovnovollem3  47107  iinhoiicclem  47122  iinhoiicc  47123  vonioolem2  47130  vonioo  47131  vonicclem2  47133  vonicc  47134