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

Theorem ixpeq2dv 8163
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 473 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32ixpeq2dva 8162 1 (𝜑X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157  Xcixp 8147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-in 3775  df-ss 3782  df-ixp 8148
This theorem is referenced by:  prdsval  16427  brssc  16785  isfunc  16835  natfval  16917  isnat  16918  dprdval  18715  elpt  21701  elptr  21702  dfac14  21747  hoicvrrex  41505  ovncvrrp  41513  ovnsubaddlem1  41519  ovnsubadd  41521  hoidmvlelem3  41546  hoidmvle  41549  ovnhoilem1  41550  ovnhoilem2  41551  ovnhoi  41552  hspval  41558  ovncvr2  41560  hspmbllem2  41576  hspmbl  41578  hoimbl  41580  opnvonmbl  41583  ovnovollem1  41605  ovnovollem3  41607  iinhoiicclem  41622  iinhoiicc  41623  vonioolem2  41630  vonioo  41631  vonicclem2  41633  vonicc  41634
  Copyright terms: Public domain W3C validator