Metamath Proof Explorer

Theorem dfrn3

Description: Alternate definition of range. Definition 6.5(2) of TakeutiZaring p. 24. (Contributed by NM, 28-Dec-1996)

Ref Expression
Assertion dfrn3 
|- ran A = { y | E. x <. x , y >. e. A }

Proof

Step Hyp Ref Expression
1 dfrn2 
 |-  ran A = { y | E. x x A y }
2 df-br 
 |-  ( x A y <-> <. x , y >. e. A )
3 2 exbii 
 |-  ( E. x x A y <-> E. x <. x , y >. e. A )
4 3 abbii 
 |-  { y | E. x x A y } = { y | E. x <. x , y >. e. A }
5 1 4 eqtri 
 |-  ran A = { y | E. x <. x , y >. e. A }