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

Theorem ixpeq2dva 7867
 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 2960 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
3 ixpeq2 7866 . 2 (∀𝑥𝐴 𝐵 = 𝐶X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
42, 3syl 17 1 (𝜑X𝑥𝐴 𝐵 = X𝑥𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  Xcixp 7852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-in 3562  df-ss 3569  df-ixp 7853 This theorem is referenced by:  ixpeq2dv  7868  dfac9  8902  xpsfrn2  16151  xpslem  16154  funcpropd  16481  natpropd  16557  prdsmgp  18531  frlmip  20036  elptr2  21287  dfac14  21331  xkoptsub  21367  prdsxmslem2  22244  rrxip  23086  ptrest  33037  prdsbnd2  33223  hoidmvlelem3  40115  ovnhoilem1  40119  ovnhoilem2  40120  hoicoto2  40123  ovnlecvr2  40128  ovncvr2  40129  ovnovollem1  40174  ovnovollem2  40175  hoimbl2  40183  vonhoire  40190  iccvonmbllem  40196  vonioolem2  40199  vonicclem2  40202  vonn0ioo2  40208  vonn0icc2  40210
 Copyright terms: Public domain W3C validator