Metamath Proof Explorer

Theorem dfrel3

Description: Alternate definition of relation. (Contributed by NM, 14-May-2008)

Ref Expression
Assertion dfrel3 
|- ( Rel R <-> ( R |` _V ) = R )

Proof

Step Hyp Ref Expression
1 dfrel2 
 |-  ( Rel R <-> `' `' R = R )
2 cnvcnv2 
 |-  `' `' R = ( R |` _V )
3 2 eqeq1i 
 |-  ( `' `' R = R <-> ( R |` _V ) = R )
4 1 3 bitri 
 |-  ( Rel R <-> ( R |` _V ) = R )