Metamath Proof Explorer

Theorem raldmqseu

Description: Equivalence between "exactly one" on the quotient carrier and "at most one" globally. Provides a type-safe way to talk about unique representatives either as E! on the intended carrier or as a global E* statement. (Contributed by Peter Mazsa, 6-Feb-2026)

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

Proof

Step Hyp Ref Expression
1 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 )
2 ralrmo3 
 |-  ( A. u e. ( dom R /. R ) E* t e. dom R u = [ t ] R <-> A. u E* t e. dom R ( u e. ( dom R /. R ) /\ u = [ t ] R ) )
3 1 2 bitr3i 
 |-  ( A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R <-> A. u E* t e. dom R ( u e. ( dom R /. R ) /\ u = [ t ] R ) )
4 eqelb 
 |-  ( ( u = [ t ] R /\ u e. ( dom R /. R ) ) <-> ( u = [ t ] R /\ [ t ] R e. ( dom R /. R ) ) )
5 ancom 
 |-  ( ( u = [ t ] R /\ u e. ( dom R /. R ) ) <-> ( u e. ( dom R /. R ) /\ u = [ t ] R ) )
6 ancom 
 |-  ( ( u = [ t ] R /\ [ t ] R e. ( dom R /. R ) ) <-> ( [ t ] R e. ( dom R /. R ) /\ u = [ t ] R ) )
7 4 5 6 3bitr3i 
 |-  ( ( u e. ( dom R /. R ) /\ u = [ t ] R ) <-> ( [ t ] R e. ( dom R /. R ) /\ u = [ t ] R ) )
8 eceldmqs 
 |-  ( R e. V -> ( [ t ] R e. ( dom R /. R ) <-> t e. dom R ) )
9 8 anbi1d 
 |-  ( R e. V -> ( ( [ t ] R e. ( dom R /. R ) /\ u = [ t ] R ) <-> ( t e. dom R /\ u = [ t ] R ) ) )
10 7 9 bitrid 
 |-  ( R e. V -> ( ( u e. ( dom R /. R ) /\ u = [ t ] R ) <-> ( t e. dom R /\ u = [ t ] R ) ) )
11 10 rmobidv 
 |-  ( R e. V -> ( E* t e. dom R ( u e. ( dom R /. R ) /\ u = [ t ] R ) <-> E* t e. dom R ( t e. dom R /\ u = [ t ] R ) ) )
12 rmoanid 
 |-  ( E* t e. dom R ( t e. dom R /\ u = [ t ] R ) <-> E* t e. dom R u = [ t ] R )
13 11 12 bitrdi 
 |-  ( R e. V -> ( E* t e. dom R ( u e. ( dom R /. R ) /\ u = [ t ] R ) <-> E* t e. dom R u = [ t ] R ) )
14 13 albidv 
 |-  ( R e. V -> ( A. u E* t e. dom R ( u e. ( dom R /. R ) /\ u = [ t ] R ) <-> A. u E* t e. dom R u = [ t ] R ) )
15 3 14 bitrid 
 |-  ( R e. V -> ( A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R <-> A. u E* t e. dom R u = [ t ] R ) )