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 e. V -> ( R e. ( RefRels i^i SymRels ) <-> ( RefRel R /\ SymRel R ) ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( R e. ( RefRels i^i SymRels ) <-> ( R e. RefRels /\ R e. SymRels ) )
2		elrefrelsrel	|- ( R e. V -> ( R e. RefRels <-> RefRel R ) )
3		elsymrelsrel	|- ( R e. V -> ( R e. SymRels <-> SymRel R ) )
4	2 3	anbi12d	|- ( R e. V -> ( ( R e. RefRels /\ R e. SymRels ) <-> ( RefRel R /\ SymRel R ) ) )
5	1 4	syl5bb	|- ( R e. V -> ( R e. ( RefRels i^i SymRels ) <-> ( RefRel R /\ SymRel R ) ) )