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 R V R RefRels SymRels RefRel R SymRel R

Proof

Step Hyp Ref Expression
1 elin R RefRels SymRels R RefRels R SymRels
2 elrefrelsrel R V R RefRels RefRel R
3 elsymrelsrel R V R SymRels SymRel R
4 2 3 anbi12d R V R RefRels R SymRels RefRel R SymRel R
5 1 4 syl5bb R V R RefRels SymRels RefRel R SymRel R