Theorem intimass

Description: The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimass	|- ( |^| A " B ) C_ |^| { x | E. a e. A x = ( a " B ) }

Proof

Step	Hyp	Ref	Expression
1		r19.12	|- ( E. b e. B A. a e. A <. b , y >. e. a -> A. a e. A E. b e. B <. b , y >. e. a )
2		elimaint	|- ( y e. ( |^| A " B ) <-> E. b e. B A. a e. A <. b , y >. e. a )
3		elintima	|- ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. a e. A E. b e. B <. b , y >. e. a )
4	1 2 3	3imtr4i	|- ( y e. ( |^| A " B ) -> y e. |^| { x | E. a e. A x = ( a " B ) } )
5	4	ssriv	|- ( |^| A " B ) C_ |^| { x | E. a e. A x = ( a " B ) }