Theorem dmqscoelseq

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	dmqscoelseq	|- ( ( dom ~ A /. ~ A ) = A <-> ( U. A /. ~ A ) = A )

Proof

Step	Hyp	Ref	Expression
1		dmcoels	|- dom ~ A = U. A
2	1	qseq1i	|- ( dom ~ A /. ~ A ) = ( U. A /. ~ A )
3	2	eqeq1i	|- ( ( dom ~ A /. ~ A ) = A <-> ( U. A /. ~ A ) = A )