This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfsymrel2

Description: Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 19-Apr-2019) (Revised by Peter Mazsa, 17-Aug-2021)

Ref Expression
Assertion dfsymrel2 
|- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 df-symrel 
 |-  ( SymRel R <-> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )
2 dfrel6 
 |-  ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R )
3 2 biimpi 
 |-  ( Rel R -> ( R i^i ( dom R X. ran R ) ) = R )
4 3 cnveqd 
 |-  ( Rel R -> `' ( R i^i ( dom R X. ran R ) ) = `' R )
5 4 3 sseq12d 
 |-  ( Rel R -> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) <-> `' R C_ R ) )
6 5 pm5.32ri 
 |-  ( ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) <-> ( `' R C_ R /\ Rel R ) )
7 1 6 bitri 
 |-  ( SymRel R <-> ( `' R C_ R /\ Rel R ) )