Theorem foelrn

Description: Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011)

	Ref	Expression
Assertion	foelrn	|- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) )

Proof

Step	Hyp	Ref	Expression
1		dffo3	|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
2	1	simprbi	|- ( F : A -onto-> B -> A. y e. B E. x e. A y = ( F ` x ) )
3		eqeq1	|- ( y = C -> ( y = ( F ` x ) <-> C = ( F ` x ) ) )
4	3	rexbidv	|- ( y = C -> ( E. x e. A y = ( F ` x ) <-> E. x e. A C = ( F ` x ) ) )
5	4	rspccva	|- ( ( A. y e. B E. x e. A y = ( F ` x ) /\ C e. B ) -> E. x e. A C = ( F ` x ) )
6	2 5	sylan	|- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) )