Metamath Proof Explorer

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 ⊢ ∀ u ∈ dom ⁡ R / R ∃* t ∈ dom ⁡ R u = t R ↔ ∀ u ∈ dom ⁡ R / R ∃! t ∈ dom ⁡ R u = t R

Proof

Step Hyp Ref Expression
1 df-qs ⊢ dom ⁡ R / R = u | ∃ t ∈ dom ⁡ R u = t R
2 1 eqabri ⊢ u ∈ dom ⁡ R / R ↔ ∃ t ∈ dom ⁡ R u = t R
3 2 biimpi ⊢ u ∈ dom ⁡ R / R → ∃ t ∈ dom ⁡ R u = t R
4 3 biantrurd ⊢ u ∈ dom ⁡ R / R → ∃* t ∈ dom ⁡ R u = t R ↔ ∃ t ∈ dom ⁡ R u = t R ∧ ∃* t ∈ dom ⁡ R u = t R
5 reu5 ⊢ ∃! t ∈ dom ⁡ R u = t R ↔ ∃ t ∈ dom ⁡ R u = t R ∧ ∃* t ∈ dom ⁡ R u = t R
6 4 5 bitr4di ⊢ u ∈ dom ⁡ R / R → ∃* t ∈ dom ⁡ R u = t R ↔ ∃! t ∈ dom ⁡ R u = t R
7 6 ralbiia ⊢ ∀ u ∈ dom ⁡ R / R ∃* t ∈ dom ⁡ R u = t R ↔ ∀ u ∈ dom ⁡ R / R ∃! t ∈ dom ⁡ R u = t R