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 )