Theorem ss2ixp 7494

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 3503	. . . . 5 |- ( B C_ C -> ( ( f ` x ) e. B -> ( f ` x ) e. C ) )
2	1	ral2imi 2855	. . . 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 3578	. 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 7482	. 2 |- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
6		df-ixp 7482	. 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 3550	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 1767   {cab 2452   A.wral 2817   C_ wss 3481   Fn wfn 5589   ` cfv 5594   X_cixp 7481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-in 3488  df-ss 3495  df-ixp 7482

This theorem is referenced by:  ixpeq2  7495  boxcutc  7524  pwcfsdom  8970  prdsval  14727  prdshom  14739  sscpwex  15062  wunfunc  15143  wunnat  15200  dprdss  16948  psrbaglefi  17893  psrbaglefiOLD  17894  ptuni2  19945  ptcld  19982  ptclsg  19984  prdstopn  19997  xkopt  20024  tmdgsum2  20463  ressprdsds  20742  prdsbl  20862  prdstotbnd  30208