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	⊢ Ⅎ 𝑥 𝐴
	fvelrnbf.2	⊢ Ⅎ 𝑥 𝐵
	fvelrnbf.3	⊢ Ⅎ 𝑥 𝐹
Assertion	fvelrnbf	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fvelrnbf.1	⊢ Ⅎ 𝑥 𝐴
2		fvelrnbf.2	⊢ Ⅎ 𝑥 𝐵
3		fvelrnbf.3	⊢ Ⅎ 𝑥 𝐹
4		fvelrnb	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = 𝐵 ) )
5		nfcv	⊢ Ⅎ 𝑦 𝐴
6		nfcv	⊢ Ⅎ 𝑥 𝑦
7	3 6	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
8	7 2	nfeq	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝐵
9		nfv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) = 𝐵
10		fveqeq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝐵 ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
11	5 1 8 9 10	cbvrexfw	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 )
12	4 11	bitrdi	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )