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

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
StepHypRef Expression
1 ixpeq2dv.1 . . 3 (𝜑𝐵 = 𝐶)
21adantr 480 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32ixpeq2dva 8952 1 (𝜑X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator