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

Theorem ixpeq2dva 7486
Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
ixpeq2dva.1  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
Assertion
Ref Expression
ixpeq2dva  |-  ( ph  -> 
X_ x  e.  A  B  =  X_ x  e.  A  C )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)

Proof of Theorem ixpeq2dva
StepHypRef Expression
1 ixpeq2dva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
21ralrimiva 2857 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
3 ixpeq2 7485 . 2  |-  ( A. x  e.  A  B  =  C  ->  X_ x  e.  A  B  =  X_ x  e.  A  C
)
42, 3syl 16 1  |-  ( ph  -> 
X_ x  e.  A  B  =  X_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   A.wral 2793   X_cixp 7471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-in 3468  df-ss 3475  df-ixp 7472
This theorem is referenced by:  ixpeq2dv  7487  dfac9  8519  xpsfrn2  14844  xpslem  14847  funcpropd  15143  natpropd  15219  prdsmgp  17133  frlmip  18682  elptr2  19948  dfac14  19992  xkoptsub  20028  prdsxmslem2  20905  rrxip  21695  ptrest  30023  prdsbnd2  30266
  Copyright terms: Public domain W3C validator