Theorem ixpeq2dv 8909

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  Xcixp 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-v 3474  df-in 3954  df-ss 3964  df-ixp 8894

This theorem is referenced by:  prdsval  17405  brssc  17765  isfunc  17818  natfval  17901  isnat  17902  dprdval  19914  elpt  23296  elptr  23297  dfac14  23342  hoicvrrex  45570  ovncvrrp  45578  ovnsubaddlem1  45584  ovnsubadd  45586  hoidmvlelem3  45611  hoidmvle  45614  ovnhoilem1  45615  ovnhoilem2  45616  ovnhoi  45617  hspval  45623  ovncvr2  45625  hspmbllem2  45641  hspmbl  45643  hoimbl  45645  opnvonmbl  45648  ovnovollem1  45670  ovnovollem3  45672  iinhoiicclem  45687  iinhoiicc  45688  vonioolem2  45695  vonioo  45696  vonicclem2  45698  vonicc  45699