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

Theorem ss2ixp 7502
 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 3497 . . . . 5
21ral2imi 2845 . . . 4
32anim2d 565 . . 3
43ss2abdv 3572 . 2
5 df-ixp 7490 . 2
6 df-ixp 7490 . 2
74, 5, 63sstr4g 3544 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  {cab 2442  A.wral 2807  C_wss 3475  Fnwfn 5588  cfv 5593  X_`cixp 7489 This theorem is referenced by:  ixpeq2  7503  boxcutc  7532  pwcfsdom  8979  prdsval  14852  prdshom  14864  sscpwex  15184  wunfunc  15268  wunnat  15325  dprdss  17076  psrbaglefi  18023  psrbaglefiOLD  18024  ptuni2  20077  ptcld  20114  ptclsg  20116  prdstopn  20129  xkopt  20156  tmdgsum2  20595  ressprdsds  20874  prdsbl  20994  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