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 bitrid ⊢ R ∈ V → R ∈ RefRels ∩ SymRels ↔ RefRel R ∧ SymRel R