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

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