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

Theorem ixpeq2dva 7378
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 2822 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
3 ixpeq2 7377 . 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 1370    e. wcel 1758   A.wral 2795   X_cixp 7363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-in 3433  df-ss 3440  df-ixp 7364
This theorem is referenced by:  ixpeq2dv  7379  dfac9  8406  xpsfrn2  14610  xpslem  14613  funcpropd  14912  natpropd  14988  prdsmgp  16808  frlmip  18312  elptr2  19263  dfac14  19307  xkoptsub  19343  prdsxmslem2  20220  rrxip  21010  ptrest  28563  prdsbnd2  28832
  Copyright terms: Public domain W3C validator