Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 ) can use the A. x e. dom R x R x version for their reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrels3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 22-Jul-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | elrefsymrels3 | |- ( R e. ( RefRels i^i SymRels ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ R e. Rels ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrefsymrels2 | |- ( R e. ( RefRels i^i SymRels ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ R e. Rels ) ) |
|
2 | idrefALT | |- ( ( _I |` dom R ) C_ R <-> A. x e. dom R x R x ) |
|
3 | cnvsym | |- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) |
|
4 | 2 3 | anbi12i | |- ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) <-> ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) ) |
5 | 4 | anbi1i | |- ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ R e. Rels ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ R e. Rels ) ) |
6 | 1 5 | bitri | |- ( R e. ( RefRels i^i SymRels ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ R e. Rels ) ) |