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 
|- 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 }