This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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