Theorem eleqvrels3

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

	Ref	Expression
Assertion	eleqvrels3	⊢ ( 𝑅 ∈ EqvRels ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dfeqvrels3	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) }
2		dmeq	⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
4	2 3	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ) )
5		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
6		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑦 𝑟 𝑥 ↔ 𝑦 𝑅 𝑥 ) )
7	5 6	imbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
8	7	2albidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
9		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑦 𝑟 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
10	5 9	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
11		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
12	10 11	imbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
13	12	2albidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
14	13	albidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
15	4 8 14	3anbi123d	⊢ ( 𝑟 = 𝑅 → ( ( ∀ 𝑥 ∈ dom 𝑟 𝑥 𝑟 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑟 𝑦 → 𝑦 𝑟 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
16	1 15	rabeqel	⊢ ( 𝑅 ∈ EqvRels ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ 𝑅 ∈ Rels ) )