Metamath Proof Explorer

Theorem dfrel5

Description: Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018)

Ref Expression
Assertion dfrel5 
|- ( Rel R <-> ( R |` dom R ) = R )

Proof

Step Hyp Ref Expression
1 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
2 resdm2 
 |-  ( R |` dom R ) = `' `' R
3 2 eqeq1i 
 |-  ( ( R |` dom R ) = R <-> `' `' R = R )
4 1 3 bitr4i 
 |-  ( Rel R <-> ( R |` dom R ) = R )