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	⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-qs	⊢ ( dom 𝑅 / 𝑅 ) = { 𝑢 ∣ ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 }
2	1	eqabri	⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
3	2	biimpi	⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) → ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
4	3	biantrurd	⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) → ( ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ( ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ∧ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) )
5		reu5	⊢ ( ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ( ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ∧ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
6	4 5	bitr4di	⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) → ( ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
7	6	ralbiia	⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )