Theorem ixpeq2dv 8088

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

Syntax hints:   → wi 4   = wceq 1630   ∈ wcel 2137  Xcixp 8072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-in 3720  df-ss 3727  df-ixp 8073

This theorem is referenced by:  prdsval  16315  brssc  16673  isfunc  16723  natfval  16805  isnat  16806  dprdval  18600  elpt  21575  elptr  21576  dfac14  21621  hoicvrrex  41274  ovncvrrp  41282  ovnsubaddlem1  41288  ovnsubadd  41290  hoidmvlelem3  41315  hoidmvle  41318  ovnhoilem1  41319  ovnhoilem2  41320  ovnhoi  41321  hspval  41327  ovncvr2  41329  hspmbllem2  41345  hspmbl  41347  hoimbl  41349  opnvonmbl  41352  ovnovollem1  41374  ovnovollem3  41376  iinhoiicclem  41391  iinhoiicc  41392  vonioolem2  41399  vonioo  41400  vonicclem2  41402  vonicc  41403