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

Theorem ss2ixp 6845
 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 3187 . . . . 5
21ral2imi 2632 . . . 4
32anim2d 548 . . 3
43ss2abdv 3259 . 2
5 df-ixp 6834 . 2
6 df-ixp 6834 . 2
74, 5, 63sstr4g 3232 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wcel 1696  cab 2282  wral 2556   wss 3165   wfn 5266  cfv 5271  cixp 6833 This theorem is referenced by:  ixpeq2  6846  boxcutc  6875  pwcfsdom  8221  prdsval  13371  prdshom  13382  sscpwex  13708  wunfunc  13789  wunnat  13846  dprdss  15280  psrbaglefi  16134  ptuni2  17287  ptcld  17323  ptclsg  17325  prdstopn  17338  xkopt  17365  tmdgsum2  17795  ressprdsds  17951  prdsbl  18053  dstr  25274  prdstotbnd  26621 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