Theorem intpreima

Description: Preimage of an intersection. (Contributed by FL, 28-Apr-2012)

	Ref	Expression
Assertion	intpreima	|- ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^| A ) = |^|_ x e. A ( `' F " x ) )

Proof

Step	Hyp	Ref	Expression
1		intiin	|- |^| A = |^|_ x e. A x
2	1	imaeq2i	|- ( `' F " |^| A ) = ( `' F " |^|_ x e. A x )
3		iinpreima	|- ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^|_ x e. A x ) = |^|_ x e. A ( `' F " x ) )
4	2 3	eqtrid	|- ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^| A ) = |^|_ x e. A ( `' F " x ) )