Metamath Proof Explorer

Theorem refsymrel3

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the A. x e. dom R x R x version for its reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrel3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 23-Aug-2021)

Ref Expression
Assertion refsymrel3 ⊢ RefRel R ∧ SymRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dfrefrel3 ⊢ RefRel R ↔ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ Rel ⁡ R
2 dfsymrel3 ⊢ SymRel R ↔ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
3 1 2 anbi12i ⊢ RefRel R ∧ SymRel R ↔ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ Rel ⁡ R ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
4 anandi3r ⊢ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ Rel ⁡ R ∧ ∀ x ∀ y x R y → y R x ↔ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ Rel ⁡ R ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
5 3anan32 ⊢ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ Rel ⁡ R ∧ ∀ x ∀ y x R y → y R x ↔ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
6 3 4 5 3bitr2i ⊢ RefRel R ∧ SymRel R ↔ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
7 symrefref3 ⊢ ∀ x ∀ y x R y → y R x → ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ↔ ∀ x ∈ dom ⁡ R x R x
8 7 pm5.32ri ⊢ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ ∀ x ∀ y x R y → y R x ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x
9 8 anbi1i ⊢ ∀ x ∈ dom ⁡ R ∀ y ∈ ran ⁡ R x = y → x R y ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
10 6 9 bitri ⊢ RefRel R ∧ SymRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R