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.)

	Ref	Expression
Assertion	refsymrels3	|- ( 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 ) ) }

Proof

Step	Hyp	Ref	Expression
1		refsymrels2	|- ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }
2		idrefALT	|- ( ( _I |` dom r ) C_ r <-> A. x e. dom r x r x )
3		cnvsym	|- ( `' r C_ r <-> A. x A. y ( x r y -> y r x ) )
4	2 3	anbi12i	|- ( ( ( _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 ) ) )
5	1 4	rabbieq	|- ( 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 ) ) }