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	⊢ Ⅎ 𝑥 𝐴
	dfrnf.2	⊢ Ⅎ 𝑦 𝐴
Assertion	dfrnf	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		dfrnf.1	⊢ Ⅎ 𝑥 𝐴
2		dfrnf.2	⊢ Ⅎ 𝑦 𝐴
3		dfrn2	⊢ ran 𝐴 = { 𝑤 ∣ ∃ 𝑣 𝑣 𝐴 𝑤 }
4		nfcv	⊢ Ⅎ 𝑥 𝑣
5		nfcv	⊢ Ⅎ 𝑥 𝑤
6	4 1 5	nfbr	⊢ Ⅎ 𝑥 𝑣 𝐴 𝑤
7		nfv	⊢ Ⅎ 𝑣 𝑥 𝐴 𝑤
8		breq1	⊢ ( 𝑣 = 𝑥 → ( 𝑣 𝐴 𝑤 ↔ 𝑥 𝐴 𝑤 ) )
9	6 7 8	cbvexv1	⊢ ( ∃ 𝑣 𝑣 𝐴 𝑤 ↔ ∃ 𝑥 𝑥 𝐴 𝑤 )
10	9	abbii	⊢ { 𝑤 ∣ ∃ 𝑣 𝑣 𝐴 𝑤 } = { 𝑤 ∣ ∃ 𝑥 𝑥 𝐴 𝑤 }
11		nfcv	⊢ Ⅎ 𝑦 𝑥
12		nfcv	⊢ Ⅎ 𝑦 𝑤
13	11 2 12	nfbr	⊢ Ⅎ 𝑦 𝑥 𝐴 𝑤
14	13	nfex	⊢ Ⅎ 𝑦 ∃ 𝑥 𝑥 𝐴 𝑤
15		nfv	⊢ Ⅎ 𝑤 ∃ 𝑥 𝑥 𝐴 𝑦
16		breq2	⊢ ( 𝑤 = 𝑦 → ( 𝑥 𝐴 𝑤 ↔ 𝑥 𝐴 𝑦 ) )
17	16	exbidv	⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 𝑥 𝐴 𝑤 ↔ ∃ 𝑥 𝑥 𝐴 𝑦 ) )
18	14 15 17	cbvabw	⊢ { 𝑤 ∣ ∃ 𝑥 𝑥 𝐴 𝑤 } = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
19	3 10 18	3eqtri	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }