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

Theorem ixpeq1d 7917
Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
ixpeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ixpeq1d (𝜑X𝑥𝐴 𝐶 = X𝑥𝐵 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem ixpeq1d
StepHypRef Expression
1 ixpeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ixpeq1 7916 . 2 (𝐴 = 𝐵X𝑥𝐴 𝐶 = X𝑥𝐵 𝐶)
31, 2syl 17 1 (𝜑X𝑥𝐴 𝐶 = X𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  Xcixp 7905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-fn 5889  df-ixp 7906
This theorem is referenced by:  elixpsn  7944  ixpsnf1o  7945  dfac9  8955  prdsval  16109  isfunc  16518  funcpropd  16554  natfval  16600  natpropd  16630  dprdval  18396  ptval  21367  dfac14  21415  ptuncnv  21604  ptunhmeo  21605  hoidmvle  40583  hoimbl  40614
  Copyright terms: Public domain W3C validator