Metamath Proof Explorer

Theorem dfrn6

Description: Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018)

Ref Expression
Assertion dfrn6 
|- ran R = { x | [ x ] `' R =/= (/) }

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran R = dom `' R
2 dfdm6 
 |-  dom `' R = { x | [ x ] `' R =/= (/) }
3 1 2 eqtri 
 |-  ran R = { x | [ x ] `' R =/= (/) }