Theorem dmqs1cosscnvepreseq

Description: Two ways to express the equality of the domain quotient of the coelements on the class A with the class A . (Contributed by Peter Mazsa, 26-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		df-coels	⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
2	1	dmqseqeq1i	⊢ ( ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ↔ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 )
3		dmqscoelseq	⊢ ( ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 )
4	2 3	bitr3i	⊢ ( ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 )