Metamath Proof Explorer

Theorem refsymrels3

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 ) can use the A. x e. dom r x r x version for their reflexive part, not just the A. x e. dom r A. y e. ran r ( x = y -> x r y ) version of dfrefrels3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 22-Jul-2019) (Proof modification is discouraged.)

|- ( RefRels i^i SymRels ) = { r e. Rels | ( A. x e. dom r x r x /\ A. x A. y ( x r y -> y r x ) ) }

 |-  ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }

 |-  ( ( _I |` dom r ) C_ r <-> A. x e. dom r x r x )

 |-  ( `' r C_ r <-> A. x A. y ( x r y -> y r x ) )

 |-  ( ( ( _I |` dom r ) C_ r /\ `' r C_ r ) <-> ( A. x e. dom r x r x /\ A. x A. y ( x r y -> y r x ) ) )

 |-  ( RefRels i^i SymRels ) = { r e. Rels | ( A. x e. dom r x r x /\ A. x A. y ( x r y -> y r x ) ) }