Metamath Proof Explorer


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 ) )