Metamath Proof Explorer


Theorem refsymrel2

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrel2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 23-Aug-2021)

Ref Expression
Assertion refsymrel2 RefRel R SymRel R I dom R R R -1 R Rel R

Proof

Step Hyp Ref Expression
1 dfrefrel2 RefRel R I dom R × ran R R Rel R
2 dfsymrel2 SymRel R R -1 R Rel R
3 1 2 anbi12i RefRel R SymRel R I dom R × ran R R Rel R R -1 R Rel R
4 anandi3r I dom R × ran R R Rel R R -1 R I dom R × ran R R Rel R R -1 R Rel R
5 3anan32 I dom R × ran R R Rel R R -1 R I dom R × ran R R R -1 R Rel R
6 3 4 5 3bitr2i RefRel R SymRel R I dom R × ran R R R -1 R Rel R
7 symrefref2 R -1 R I dom R × ran R R I dom R R
8 7 pm5.32ri I dom R × ran R R R -1 R I dom R R R -1 R
9 8 anbi1i I dom R × ran R R R -1 R Rel R I dom R R R -1 R Rel R
10 6 9 bitri RefRel R SymRel R I dom R R R -1 R Rel R