Theorem ixpeq2dv 8953

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Xcixp 8937

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-ss 3968  df-ixp 8938

This theorem is referenced by:  prdsval  17500  brssc  17858  isfunc  17909  natfval  17994  isnat  17995  dprdval  20023  elpt  23580  elptr  23581  dfac14  23626  ixpeq12dv  36217  hoicvrrex  46571  ovncvrrp  46579  ovnsubaddlem1  46585  ovnsubadd  46587  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem1  46616  ovnhoilem2  46617  ovnhoi  46618  hspval  46624  ovncvr2  46626  hspmbllem2  46642  hspmbl  46644  hoimbl  46646  opnvonmbl  46649  ovnovollem1  46671  ovnovollem3  46673  iinhoiicclem  46688  iinhoiicc  46689  vonioolem2  46696  vonioo  46697  vonicclem2  46699  vonicc  46700