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 \in V \to (R \in (RefRels \cap SymRels) \leftrightarrow (RefRel R \land SymRel R))$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ R \in (RefRels \cap SymRels) \leftrightarrow (R \in RefRels \land R \in SymRels)$
2		elrefrelsrel	$⊢ R \in V \to (R \in RefRels \leftrightarrow RefRel R)$
3		elsymrelsrel	$⊢ R \in V \to (R \in SymRels \leftrightarrow SymRel R)$
4	2 3	anbi12d	$⊢ R \in V \to ((R \in RefRels \land R \in SymRels) \leftrightarrow (RefRel R \land SymRel R))$
5	1 4	syl5bb	$⊢ R \in V \to (R \in (RefRels \cap SymRels) \leftrightarrow (RefRel R \land SymRel R))$