Theorem raldmqsmo

Description: On the quotient carrier, "at most one" and "exactly one" coincide for coset witnesses. (Contributed by Peter Mazsa, 6-Feb-2026)

	Ref	Expression
Assertion	raldmqsmo	|- ( A. u e. ( dom R /. R ) E* t e. dom R u = [ t ] R <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R )

Proof

Step	Hyp	Ref	Expression
1		df-qs	|- ( dom R /. R ) = { u | E. t e. dom R u = [ t ] R }
2	1	eqabri	|- ( u e. ( dom R /. R ) <-> E. t e. dom R u = [ t ] R )
3	2	biimpi	|- ( u e. ( dom R /. R ) -> E. t e. dom R u = [ t ] R )
4	3	biantrurd	|- ( u e. ( dom R /. R ) -> ( E* t e. dom R u = [ t ] R <-> ( E. t e. dom R u = [ t ] R /\ E* t e. dom R u = [ t ] R ) ) )
5		reu5	|- ( E! t e. dom R u = [ t ] R <-> ( E. t e. dom R u = [ t ] R /\ E* t e. dom R u = [ t ] R ) )
6	4 5	bitr4di	|- ( u e. ( dom R /. R ) -> ( E* t e. dom R u = [ t ] R <-> E! t e. dom R u = [ t ] R ) )
7	6	ralbiia	|- ( A. u e. ( dom R /. R ) E* t e. dom R u = [ t ] R <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R )