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 =/= (/) }