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

Theorem ss2ixp 7535
 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 3455 . . . . 5
21ral2imi 2811 . . . 4
32anim2d 567 . . 3
43ss2abdv 3531 . 2
5 df-ixp 7523 . 2
6 df-ixp 7523 . 2
74, 5, 63sstr4g 3502 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wcel 1867  cab 2405  wral 2773   wss 3433   wfn 5588  cfv 5593  cixp 7522 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-in 3440  df-ss 3447  df-ixp 7523 This theorem is referenced by:  ixpeq2  7536  boxcutc  7565  pwcfsdom  9004  prdsval  15331  prdshom  15343  sscpwex  15698  wunfunc  15782  wunnat  15839  dprdss  17640  psrbaglefi  18574  ptuni2  20568  ptcld  20605  ptclsg  20607  prdstopn  20620  xkopt  20647  tmdgsum2  21088  ressprdsds  21363  prdsbl  21483  ptrecube  31848  prdstotbnd  32034
 Copyright terms: Public domain W3C validator