Theorem eqvreldmqs2

Description: Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 30-Dec-2024)

	Ref	Expression
Assertion	eqvreldmqs2	⊢ ( ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ∧ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-coels	⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
2	1	eqvreleqi	⊢ ( EqvRel ∼ 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )
3	2	bicomi	⊢ ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ↔ EqvRel ∼ 𝐴 )
4		dmqs1cosscnvepreseq	⊢ ( ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 )
5	3 4	anbi12i	⊢ ( ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ∧ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )