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

Theorem ixpeq2 7503
 Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
ixpeq2

Proof of Theorem ixpeq2
StepHypRef Expression
1 ss2ixp 7502 . . 3
2 ss2ixp 7502 . . 3
31, 2anim12i 566 . 2
4 eqss 3518 . . . 4
54ralbii 2888 . . 3
6 r19.26 2984 . . 3
75, 6bitri 249 . 2
8 eqss 3518 . 2
93, 7, 83imtr4i 266 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  A.wral 2807  C_wss 3475  X_cixp 7489 This theorem is referenced by:  ixpeq2dva  7504  ixpint  7516  prdsbas3  14878  pwsbas  14884  ptbasfi  20082  ptunimpt  20096  pttopon  20097  ptcld  20114  ptrescn  20140  ptuncnv  20308  ptunhmeo  20309  ptrest  30048  prdstotbnd  30290 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-in 3482  df-ss 3489  df-ixp 7490
 Copyright terms: Public domain W3C validator