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

Metamath Proof Explorer

Theorem symrefref3

Description: Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 . (Contributed by Peter Mazsa, 23-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Assertion symrefref3 
|- ( A. x A. y ( x R y -> y R x ) -> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) )

Proof

Step Hyp Ref Expression
1 symrefref2 
 |-  ( `' R C_ R -> ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) )
2 cnvsym 
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
3 idinxpss 
 |-  ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> A. x e. dom R A. y e. ran R ( x = y -> x R y ) )
4 idrefALT 
 |-  ( ( _I |` dom R ) C_ R <-> A. x e. dom R x R x )
5 3 4 bibi12i 
 |-  ( ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) )
6 1 2 5 3imtr3i 
 |-  ( A. x A. y ( x R y -> y R x ) -> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) )