Metamath Proof Explorer

Theorem eleqvrels3

Description: Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021)

Ref Expression
Assertion eleqvrels3 ⊢ R ∈ EqvRels ↔ ∀ 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 ∧ R ∈ Rels

Proof

Step Hyp Ref Expression
1 dfeqvrels3 ⊢ EqvRels = r ∈ Rels | ∀ 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
2 dmeq ⊢ r = R → dom ⁡ r = dom ⁡ R
3 breq ⊢ r = R → x r x ↔ x R x
4 2 3 raleqbidv ⊢ r = R → ∀ x ∈ dom ⁡ r x r x ↔ ∀ x ∈ dom ⁡ R x R x
5 breq ⊢ r = R → x r y ↔ x R y
6 breq ⊢ r = R → y r x ↔ y R x
7 5 6 imbi12d ⊢ r = R → x r y → y r x ↔ x R y → y R x
8 7 2albidv ⊢ r = R → ∀ x ∀ y x r y → y r x ↔ ∀ x ∀ y x R y → y R x
9 breq ⊢ r = R → y r z ↔ y R z
10 5 9 anbi12d ⊢ r = R → x r y ∧ y r z ↔ x R y ∧ y R z
11 breq ⊢ r = R → x r z ↔ x R z
12 10 11 imbi12d ⊢ r = R → x r y ∧ y r z → x r z ↔ x R y ∧ y R z → x R z
13 12 2albidv ⊢ r = R → ∀ y ∀ z x r y ∧ y r z → x r z ↔ ∀ y ∀ z x R y ∧ y R z → x R z
14 13 albidv ⊢ r = R → ∀ x ∀ y ∀ z x r y ∧ y r z → x r z ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z
15 4 8 14 3anbi123d ⊢ r = 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 ↔ ∀ 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
16 1 15 rabeqel ⊢ R ∈ EqvRels ↔ ∀ 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 ∧ R ∈ Rels