This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 )