This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }