Theorem ss2ixp

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

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

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( B C_ C -> ( ( f ` x ) e. B -> ( f ` x ) e. C ) )
2	1	ral2imi	|- ( 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	|- ( 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	|- ( 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	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
6		df-ixp	|- 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	|- ( A. x e. A B C_ C -> X_ x e. A B C_ X_ x e. A C )