Theorem foelrnf

Description: Property of a surjective function. As foelrn but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

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