Theorem eqvreldmqs

Description: Two ways to express membership equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 26-Sep-2021) (Revised by Peter Mazsa, 17-Jul-2023)

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

Proof

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