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	|- F/_ x A
	dfrnf.2	|- F/_ y A
Assertion	dfrnf	|- ran A = { y | E. x x A y }

Proof

Step	Hyp	Ref	Expression
1		dfrnf.1	|- F/_ x A
2		dfrnf.2	|- F/_ y A
3		dfrn2	|- ran A = { w | E. v v A w }
4		nfcv	|- F/_ x v
5		nfcv	|- F/_ x w
6	4 1 5	nfbr	|- F/ x v A w
7		nfv	|- F/ v x A w
8		breq1	|- ( v = x -> ( v A w <-> x A w ) )
9	6 7 8	cbvexv1	|- ( E. v v A w <-> E. x x A w )
10	9	abbii	|- { w | E. v v A w } = { w | E. x x A w }
11		nfcv	|- F/_ y x
12		nfcv	|- F/_ y w
13	11 2 12	nfbr	|- F/ y x A w
14	13	nfex	|- F/ y E. x x A w
15		nfv	|- F/ w E. x x A y
16		breq2	|- ( w = y -> ( x A w <-> x A y ) )
17	16	exbidv	|- ( w = y -> ( E. x x A w <-> E. x x A y ) )
18	14 15 17	cbvabw	|- { w | E. x x A w } = { y | E. x x A y }
19	3 10 18	3eqtri	|- ran A = { y | E. x x A y }