Theorem ixpeq2dv 7810

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Xcixp 7794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-in 3547  df-ss 3554  df-ixp 7795

This theorem is referenced by:  prdsval  15938  brssc  16297  isfunc  16347  natfval  16429  isnat  16430  dprdval  18225  elpt  21185  elptr  21186  dfac14  21231  hoicvrrex  39446  ovncvrrp  39454  ovnsubaddlem1  39460  ovnsubadd  39462  hoidmvlelem3  39487  hoidmvle  39490  ovnhoilem1  39491  ovnhoilem2  39492  ovnhoi  39493  hspval  39499  ovncvr2  39501  hspmbllem2  39517  hspmbl  39519  hoimbl  39521  opnvonmbl  39524  ovnovollem1  39546  ovnovollem3  39548  iinhoiicclem  39564  iinhoiicc  39565  vonioolem2  39572  vonioo  39573  vonicclem2  39575  vonicc  39576