Metamath Proof Explorer

Theorem dfrel2

Description: Alternate definition of relation. Exercise 2 of TakeutiZaring p. 25. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dfrel2 
|- ( Rel R <-> `' `' R = R )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' `' R
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 opelcnv 
 |-  ( <. x , y >. e. `' `' R <-> <. y , x >. e. `' R )
5 3 2 opelcnv 
 |-  ( <. y , x >. e. `' R <-> <. x , y >. e. R )
6 4 5 bitri 
 |-  ( <. x , y >. e. `' `' R <-> <. x , y >. e. R )
7 6 eqrelriv 
 |-  ( ( Rel `' `' R /\ Rel R ) -> `' `' R = R )
8 1 7 mpan 
 |-  ( Rel R -> `' `' R = R )
9 releq 
 |-  ( `' `' R = R -> ( Rel `' `' R <-> Rel R ) )
10 1 9 mpbii 
 |-  ( `' `' R = R -> Rel R )
11 8 10 impbii 
 |-  ( Rel R <-> `' `' R = R )