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	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( 𝑅 ∈ RefRels ∧ 𝑅 ∈ SymRels ) )
2		elrefrelsrel	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ RefRels ↔ RefRel 𝑅 ) )
3		elsymrelsrel	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ SymRels ↔ SymRel 𝑅 ) )
4	2 3	anbi12d	⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ∈ RefRels ∧ 𝑅 ∈ SymRels ) ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) )
5	1 4	bitrid	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) )