Metamath Proof Explorer

Theorem ralmo

Description: "At most one" can be restricted to the range. (Contributed by Peter Mazsa, 2-Feb-2026)

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

Proof

Step Hyp Ref Expression
1 brelrng 
 |-  ( ( u e. _V /\ x e. _V /\ u R x ) -> x e. ran R )
2 1 el3v12 
 |-  ( u R x -> x e. ran R )
3 2 pm4.71ri 
 |-  ( u R x <-> ( x e. ran R /\ u R x ) )
4 3 mobii 
 |-  ( E* u u R x <-> E* u ( x e. ran R /\ u R x ) )
5 moanimv 
 |-  ( E* u ( x e. ran R /\ u R x ) <-> ( x e. ran R -> E* u u R x ) )
6 4 5 bitri 
 |-  ( E* u u R x <-> ( x e. ran R -> E* u u R x ) )
7 6 albii 
 |-  ( A. x E* u u R x <-> A. x ( x e. ran R -> E* u u R x ) )
8 df-ral 
 |-  ( A. x e. ran R E* u u R x <-> A. x ( x e. ran R -> E* u u R x ) )
9 7 8 bitr4i 
 |-  ( A. x E* u u R x <-> A. x e. ran R E* u u R x )