Theorem ixpeq2dv 8979

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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	ixpeq2dva 8978	1 ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Xcixp 8963

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-ss 3901  df-ixp 8964

This theorem is used by:  prdsval  17676  brssc  18039  isfunc  18089  natfval  18174  isnat  18175  dprdval  20270  elpt  23946  elptr  23947  dfac14  23992  ixpeq12dv  37220  hoicvrrex  47839  ovncvrrp  47847  ovnsubaddlem1  47853  ovnsubadd  47855  hoidmvlelem3  47880  hoidmvle  47883  ovnhoilem1  47884  ovnhoilem2  47885  ovnhoi  47886  hspval  47892  ovncvr2  47894  hspmbllem2  47910  hspmbl  47912  hoimbl  47914  opnvonmbl  47917  ovnovollem1  47939  ovnovollem3  47941  iinhoiicclem  47956  iinhoiicc  47957  vonioolem2  47964  vonioo  47965  vonicclem2  47967  vonicc  47968