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	$$⊢\underset{\_}{Ⅎ}xA$$
	fvelrnbf.2	$$⊢\underset{\_}{Ⅎ}xB$$
	fvelrnbf.3	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	fvelrnbf	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow \exists x\in AF\left(x\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvelrnbf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		fvelrnbf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		fvelrnbf.3	$$⊢\underset{\_}{Ⅎ}xF$$
4		fvelrnb	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow \exists y\in AF\left(y\right)=B\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
7	3 6	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
8	7 2	nfeq	$$⊢ℲxF\left(y\right)=B$$
9		nfv	$$⊢ℲyF\left(x\right)=B$$
10		fveqeq2	$$⊢y=x\to \left(F\left(y\right)=B\leftrightarrow F\left(x\right)=B\right)$$
11	5 1 8 9 10	cbvrexfw	$$⊢\exists y\in AF\left(y\right)=B\leftrightarrow \exists x\in AF\left(x\right)=B$$
12	4 11	bitrdi	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow \exists x\in AF\left(x\right)=B\right)$$