Theorem fvelrnbf

Description: A version of fvelrnb using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fvelrnbf.1	|- F/_ x A
	fvelrnbf.2	|- F/_ x B
	fvelrnbf.3	|- F/_ x F
Assertion	fvelrnbf	|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		fvelrnbf.1	|- F/_ x A
2		fvelrnbf.2	|- F/_ x B
3		fvelrnbf.3	|- F/_ x F
4		fvelrnb	|- ( F Fn A -> ( B e. ran F <-> E. y e. A ( F ` y ) = B ) )
5		nfcv	|- F/_ y A
6		nfcv	|- F/_ x y
7	3 6	nffv	|- F/_ x ( F ` y )
8	7 2	nfeq	|- F/ x ( F ` y ) = B
9		nfv	|- F/ y ( F ` x ) = B
10		fveqeq2	|- ( y = x -> ( ( F ` y ) = B <-> ( F ` x ) = B ) )
11	5 1 8 9 10	cbvrexfw	|- ( E. y e. A ( F ` y ) = B <-> E. x e. A ( F ` x ) = B )
12	4 11	bitrdi	|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )