Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ixpeq2dv Structured version   Visualization version   GIF version

Theorem ixpeq2dv 8500
 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
StepHypRef Expression
1 ixpeq2dv.1 . . 3 (𝜑𝐵 = 𝐶)
21adantr 484 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32ixpeq2dva 8499 1 (𝜑X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Xcixp 8484 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-v 3411  df-in 3867  df-ss 3877  df-ixp 8485 This theorem is referenced by:  prdsval  16791  brssc  17148  isfunc  17198  natfval  17280  isnat  17281  dprdval  19198  elpt  22277  elptr  22278  dfac14  22323  hoicvrrex  43589  ovncvrrp  43597  ovnsubaddlem1  43603  ovnsubadd  43605  hoidmvlelem3  43630  hoidmvle  43633  ovnhoilem1  43634  ovnhoilem2  43635  ovnhoi  43636  hspval  43642  ovncvr2  43644  hspmbllem2  43660  hspmbl  43662  hoimbl  43664  opnvonmbl  43667  ovnovollem1  43689  ovnovollem3  43691  iinhoiicclem  43706  iinhoiicc  43707  vonioolem2  43714  vonioo  43715  vonicclem2  43717  vonicc  43718
 Copyright terms: Public domain W3C validator