Metamath Proof Explorer


Theorem elrefsymrelsrel

Description: For sets, being an element of the class of reflexive and symmetric relations is equivalent to satisfying the reflexive and symmetric relation predicates. (Contributed by Peter Mazsa, 23-Aug-2021)

Ref Expression
Assertion elrefsymrelsrel RVRRefRelsSymRelsRefRelRSymRelR

Proof

Step Hyp Ref Expression
1 elin RRefRelsSymRelsRRefRelsRSymRels
2 elrefrelsrel RVRRefRelsRefRelR
3 elsymrelsrel RVRSymRelsSymRelR
4 2 3 anbi12d RVRRefRelsRSymRelsRefRelRSymRelR
5 1 4 syl5bb RVRRefRelsSymRelsRefRelRSymRelR