Metamath Proof Explorer


Theorem elrefsymrels3

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 elrefsymrels3 R RefRels SymRels x dom R x R x x y x R y y R x R Rels

Proof

Step Hyp Ref Expression
1 elrefsymrels2 R RefRels SymRels I dom R R R -1 R R Rels
2 idrefALT I dom R R x dom R x R x
3 cnvsym R -1 R x y x R y y R x
4 2 3 anbi12i I dom R R R -1 R x dom R x R x x y x R y y R x
5 4 anbi1i I dom R R R -1 R R Rels x dom R x R x x y x R y y R x R Rels
6 1 5 bitri R RefRels SymRels x dom R x R x x y x R y y R x R Rels