Theorem rexrn

Description: Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013) (Revised by Mario Carneiro, 20-Aug-2014)

	Ref	Expression
Hypothesis	rexrn.1	|- ( x = ( F ` y ) -> ( ph <-> ps ) )
Assertion	rexrn	|- ( F Fn A -> ( E. x e. ran F ph <-> E. y e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		rexrn.1	|- ( x = ( F ` y ) -> ( ph <-> ps ) )
2		fvexd	|- ( ( F Fn A /\ y e. A ) -> ( F ` y ) e. _V )
3		fvelrnb	|- ( F Fn A -> ( x e. ran F <-> E. y e. A ( F ` y ) = x ) )
4		eqcom	|- ( ( F ` y ) = x <-> x = ( F ` y ) )
5	4	rexbii	|- ( E. y e. A ( F ` y ) = x <-> E. y e. A x = ( F ` y ) )
6	3 5	bitrdi	|- ( F Fn A -> ( x e. ran F <-> E. y e. A x = ( F ` y ) ) )
7	1	adantl	|- ( ( F Fn A /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
8	2 6 7	rexxfr2d	|- ( F Fn A -> ( E. x e. ran F ph <-> E. y e. A ps ) )