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

Theorem ss2ixp 7067
 Description: Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
Assertion
Ref Expression
ss2ixp

Proof of Theorem ss2ixp
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 3334 . . . . 5
21ral2imi 2774 . . . 4
32anim2d 549 . . 3
43ss2abdv 3408 . 2
5 df-ixp 7056 . 2
6 df-ixp 7056 . 2
74, 5, 63sstr4g 3381 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wcel 1725  cab 2421  wral 2697   wss 3312   wfn 5441  cfv 5446  cixp 7055 This theorem is referenced by:  ixpeq2  7068  boxcutc  7097  pwcfsdom  8450  prdsval  13670  prdshom  13681  sscpwex  14007  wunfunc  14088  wunnat  14145  dprdss  15579  psrbaglefi  16429  ptuni2  17600  ptcld  17637  ptclsg  17639  prdstopn  17652  xkopt  17679  tmdgsum2  18118  ressprdsds  18393  prdsbl  18513  prdstotbnd  26494 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-in 3319  df-ss 3326  df-ixp 7056
 Copyright terms: Public domain W3C validator