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

Theorem ixpeq2 6846
Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
ixpeq2  |-  ( A. x  e.  A  B  =  C  ->  X_ x  e.  A  B  =  X_ x  e.  A  C
)

Proof of Theorem ixpeq2
StepHypRef Expression
1 ss2ixp 6845 . . 3  |-  ( A. x  e.  A  B  C_  C  ->  X_ x  e.  A  B  C_  X_ x  e.  A  C )
2 ss2ixp 6845 . . 3  |-  ( A. x  e.  A  C  C_  B  ->  X_ x  e.  A  C  C_  X_ x  e.  A  B )
31, 2anim12i 549 . 2  |-  ( ( A. x  e.  A  B  C_  C  /\  A. x  e.  A  C  C_  B )  ->  ( X_ x  e.  A  B  C_  X_ x  e.  A  C  /\  X_ x  e.  A  C  C_  X_ x  e.  A  B ) )
4 eqss 3207 . . . 4  |-  ( B  =  C  <->  ( B  C_  C  /\  C  C_  B ) )
54ralbii 2580 . . 3  |-  ( A. x  e.  A  B  =  C  <->  A. x  e.  A  ( B  C_  C  /\  C  C_  B ) )
6 r19.26 2688 . . 3  |-  ( A. x  e.  A  ( B  C_  C  /\  C  C_  B )  <->  ( A. x  e.  A  B  C_  C  /\  A. x  e.  A  C  C_  B
) )
75, 6bitri 240 . 2  |-  ( A. x  e.  A  B  =  C  <->  ( A. x  e.  A  B  C_  C  /\  A. x  e.  A  C  C_  B ) )
8 eqss 3207 . 2  |-  ( X_ x  e.  A  B  =  X_ x  e.  A  C 
<->  ( X_ x  e.  A  B  C_  X_ x  e.  A  C  /\  X_ x  e.  A  C  C_  X_ x  e.  A  B ) )
93, 7, 83imtr4i 257 1  |-  ( A. x  e.  A  B  =  C  ->  X_ x  e.  A  B  =  X_ x  e.  A  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632   A.wral 2556    C_ wss 3165   X_cixp 6833
This theorem is referenced by:  ixpeq2dva  6847  ixpint  6859  dfac9  7778  prdsbas3  13396  pwsbas  13402  xpsfrn2  13488  xpslem  13491  dprdval  15254  prdsmgp  15409  elpt  17283  elptr  17284  elptr2  17285  ptbasfi  17292  ptunimpt  17306  pttopon  17307  ptcld  17323  dfac14  17328  ptrescn  17349  xkoptsub  17364  ptuncnv  17514  ptunhmeo  17515  prdsxmslem2  18091  istopx  25650  istopxc  25651  prdstotbnd  26621  prdsbnd2  26622
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-in 3172  df-ss 3179  df-ixp 6834
  Copyright terms: Public domain W3C validator