Metamath Proof Explorer

Theorem dfrn2

Description: Alternate definition of range. Definition 4 of Suppes p. 60. (Contributed by NM, 27-Dec-1996)

Ref Expression
Assertion dfrn2 
|- ran A = { y | E. x x A y }

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran A = dom `' A
2 df-dm 
 |-  dom `' A = { y | E. x y `' A x }
3 vex 
 |-  y e. _V
4 vex 
 |-  x e. _V
5 3 4 brcnv 
 |-  ( y `' A x <-> x A y )
6 5 exbii 
 |-  ( E. x y `' A x <-> E. x x A y )
7 6 abbii 
 |-  { y | E. x y `' A x } = { y | E. x x A y }
8 1 2 7 3eqtri 
 |-  ran A = { y | E. x x A y }