Theorem ixpeq2dv 8837

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Xcixp 8821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-ss 3914  df-ixp 8822

This theorem is referenced by:  prdsval  17359  brssc  17721  isfunc  17771  natfval  17856  isnat  17857  dprdval  19917  elpt  23487  elptr  23488  dfac14  23533  ixpeq12dv  36258  hoicvrrex  46602  ovncvrrp  46610  ovnsubaddlem1  46616  ovnsubadd  46618  hoidmvlelem3  46643  hoidmvle  46646  ovnhoilem1  46647  ovnhoilem2  46648  ovnhoi  46649  hspval  46655  ovncvr2  46657  hspmbllem2  46673  hspmbl  46675  hoimbl  46677  opnvonmbl  46680  ovnovollem1  46702  ovnovollem3  46704  iinhoiicclem  46719  iinhoiicc  46720  vonioolem2  46727  vonioo  46728  vonicclem2  46730  vonicc  46731