Theorem ss2ixp 7484

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

Assertion

Ref	Expression
ss2ixp	|- ( A. x e. A B C_ C -> X_ x e. A B C_ X_ x e. A C )

Proof of Theorem ss2ixp

Dummy variable f is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3483	. . . . 5 |- ( B C_ C -> ( ( f ` x ) e. B -> ( f ` x ) e. C ) )
2	1	ral2imi 2831	. . . 4 |- ( A. x e. A B C_ C -> ( A. x e. A ( f ` x ) e. B -> A. x e. A ( f ` x ) e. C ) )
3	2	anim2d 565	. . 3 |- ( A. x e. A B C_ C -> ( ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) -> ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) ) )
4	3	ss2abdv 3558	. 2 |- ( A. x e. A B C_ C -> { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) } C_ { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) } )
5		df-ixp 7472	. 2 |- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
6		df-ixp 7472	. 2 |- X_ x e. A C = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) }
7	4, 5, 6	3sstr4g 3530	1 |- ( A. x e. A B C_ C -> X_ x e. A B C_ X_ x e. A C )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1804   {cab 2428   A.wral 2793   C_ wss 3461   Fn wfn 5573   ` cfv 5578   X_cixp 7471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-in 3468  df-ss 3475  df-ixp 7472

This theorem is referenced by:  ixpeq2  7485  boxcutc  7514  pwcfsdom  8961  prdsval  14834  prdshom  14846  sscpwex  15166  wunfunc  15247  wunnat  15304  dprdss  17055  psrbaglefi  18002  psrbaglefiOLD  18003  ptuni2  20055  ptcld  20092  ptclsg  20094  prdstopn  20107  xkopt  20134  tmdgsum2  20573  ressprdsds  20852  prdsbl  20972  prdstotbnd  30266