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

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

Proof of Theorem ixpeq2dva
StepHypRef Expression
1 ixpeq2dva.1 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
21ralrimiva 3169 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
3 ixpeq2 8449 . 2 (∀𝑥𝐴 𝐵 = 𝐶X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
42, 3syl 17 1 (𝜑X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3125  Xcixp 8435 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-v 3472  df-in 3916  df-ss 3926  df-ixp 8436 This theorem is referenced by:  ixpeq2dv  8451  dfac9  9536  xpsrnbas  16819  funcpropd  17145  natpropd  17221  prdsmgp  19335  frlmip  20894  elptr2  22154  dfac14  22198  xkoptsub  22234  prdsxmslem2  23111  rrxip  23969  ptrest  34928  prdsbnd2  35105  hoidmvlelem3  43023  ovnhoilem1  43027  ovnhoilem2  43028  hoicoto2  43031  ovnlecvr2  43036  ovncvr2  43037  ovnovollem1  43082  ovnovollem2  43083  hoimbl2  43091  vonhoire  43098  iccvonmbllem  43104  vonioolem2  43107  vonicclem2  43110  vonn0ioo2  43116  vonn0icc2  43118
 Copyright terms: Public domain W3C validator