This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfeqvrel3

Description: Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019)

Ref Expression
Assertion dfeqvrel3 ⊢ EqvRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 df-eqvrel ⊢ EqvRel R ↔ RefRel R ∧ SymRel R ∧ TrRel R
2 refsymrel3 ⊢ RefRel R ∧ SymRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R
3 dftrrel3 ⊢ TrRel R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
4 2 3 anbi12i ⊢ RefRel R ∧ SymRel R ∧ TrRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
5 df-3an ⊢ RefRel R ∧ SymRel R ∧ TrRel R ↔ RefRel R ∧ SymRel R ∧ TrRel R
6 df-3an ⊢ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z
7 6 anbi1i ⊢ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
8 3anan32 ⊢ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
9 anandi3r ⊢ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
10 7 8 9 3bitr2i ⊢ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ Rel ⁡ R ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
11 4 5 10 3bitr4i ⊢ RefRel R ∧ SymRel R ∧ TrRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R
12 1 11 bitri ⊢ EqvRel R ↔ ∀ x ∈ dom ⁡ R x R x ∧ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z ∧ Rel ⁡ R