Theorem eleqvrels2

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

	Ref	Expression
Assertion	eleqvrels2	⊢ ( 𝑅 ∈ EqvRels ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dfeqvrels2	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
2		dmeq	⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3	2	reseq2d	⊢ ( 𝑟 = 𝑅 → ( I ↾ dom 𝑟 ) = ( I ↾ dom 𝑅 ) )
4		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
5	3 4	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )
6		cnveq	⊢ ( 𝑟 = 𝑅 → ◡ 𝑟 = ◡ 𝑅 )
7	6 4	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ◡ 𝑟 ⊆ 𝑟 ↔ ◡ 𝑅 ⊆ 𝑅 ) )
8		coideq	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∘ 𝑟 ) = ( 𝑅 ∘ 𝑅 ) )
9	8 4	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) )
10	5 7 9	3anbi123d	⊢ ( 𝑟 = 𝑅 → ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ) )
11	1 10	rabeqel	⊢ ( 𝑅 ∈ EqvRels ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) )