Theorem dfrnf

Description: Definition of range, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Aug-1995) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	dfrnf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dfrnf.2	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	dfrnf	$$⊢\mathrm{ran}A=\left\{y|\exists xxAy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfrnf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dfrnf.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		dfrn2	$$⊢\mathrm{ran}A=\left\{w|\exists vvAw\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xv$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
6	4 1 5	nfbr	$$⊢ℲxvAw$$
7		nfv	$$⊢ℲvxAw$$
8		breq1	$$⊢v=x\to \left(vAw\leftrightarrow xAw\right)$$
9	6 7 8	cbvexv1	$$⊢\exists vvAw\leftrightarrow \exists xxAw$$
10	9	abbii	$$⊢\left\{w|\exists vvAw\right\}=\left\{w|\exists xxAw\right\}$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}yx$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
13	11 2 12	nfbr	$$⊢ℲyxAw$$
14	13	nfex	$$⊢Ⅎy\exists xxAw$$
15		nfv	$$⊢Ⅎw\exists xxAy$$
16		breq2	$$⊢w=y\to \left(xAw\leftrightarrow xAy\right)$$
17	16	exbidv	$$⊢w=y\to \left(\exists xxAw\leftrightarrow \exists xxAy\right)$$
18	14 15 17	cbvabw	$$⊢\left\{w|\exists xxAw\right\}=\left\{y|\exists xxAy\right\}$$
19	3 10 18	3eqtri	$$⊢\mathrm{ran}A=\left\{y|\exists xxAy\right\}$$