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.

Step	Hyp	Ref	Expression
1		ssel 3497	. . . . 5
2	1	ral2imi 2845	. . . 4
3	2	anim2d 565	. . 3
4	3	ss2abdv 3572	. 2
5		df-ixp 7490	. 2
6		df-ixp 7490	. 2
7	4, 5, 6	3sstr4g 3544	1

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