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

Metamath Proof Explorer

Theorem ralrnmo

Description: On the range, "at most one" becomes "exactly one". (Contributed by Peter Mazsa, 27-Sep-2018) (Revised by Peter Mazsa, 2-Feb-2026)

Ref Expression
Assertion ralrnmo 
|- ( A. x e. ran R E* u u R x <-> A. x e. ran R E! u u R x )

Proof

Step Hyp Ref Expression
1 dfrn2 
 |-  ran R = { x | E. u u R x }
2 1 eqabri 
 |-  ( x e. ran R <-> E. u u R x )
3 2 biimpi 
 |-  ( x e. ran R -> E. u u R x )
4 3 biantrurd 
 |-  ( x e. ran R -> ( E* u u R x <-> ( E. u u R x /\ E* u u R x ) ) )
5 4 ralbiia 
 |-  ( A. x e. ran R E* u u R x <-> A. x e. ran R ( E. u u R x /\ E* u u R x ) )
6 df-eu 
 |-  ( E! u u R x <-> ( E. u u R x /\ E* u u R x ) )
7 6 ralbii 
 |-  ( A. x e. ran R E! u u R x <-> A. x e. ran R ( E. u u R x /\ E* u u R x ) )
8 5 7 bitr4i 
 |-  ( A. x e. ran R E* u u R x <-> A. x e. ran R E! u u R x )