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	⊢ ( ∀ 𝑥 ∈ ran 𝑅 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∈ ran 𝑅 ∃! 𝑢 𝑢 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		dfrn2	⊢ ran 𝑅 = { 𝑥 ∣ ∃ 𝑢 𝑢 𝑅 𝑥 }
2	1	eqabri	⊢ ( 𝑥 ∈ ran 𝑅 ↔ ∃ 𝑢 𝑢 𝑅 𝑥 )
3	2	biimpi	⊢ ( 𝑥 ∈ ran 𝑅 → ∃ 𝑢 𝑢 𝑅 𝑥 )
4	3	biantrurd	⊢ ( 𝑥 ∈ ran 𝑅 → ( ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ( ∃ 𝑢 𝑢 𝑅 𝑥 ∧ ∃* 𝑢 𝑢 𝑅 𝑥 ) ) )
5	4	ralbiia	⊢ ( ∀ 𝑥 ∈ ran 𝑅 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∈ ran 𝑅 ( ∃ 𝑢 𝑢 𝑅 𝑥 ∧ ∃* 𝑢 𝑢 𝑅 𝑥 ) )
6		df-eu	⊢ ( ∃! 𝑢 𝑢 𝑅 𝑥 ↔ ( ∃ 𝑢 𝑢 𝑅 𝑥 ∧ ∃* 𝑢 𝑢 𝑅 𝑥 ) )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ ran 𝑅 ∃! 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∈ ran 𝑅 ( ∃ 𝑢 𝑢 𝑅 𝑥 ∧ ∃* 𝑢 𝑢 𝑅 𝑥 ) )
8	5 7	bitr4i	⊢ ( ∀ 𝑥 ∈ ran 𝑅 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∈ ran 𝑅 ∃! 𝑢 𝑢 𝑅 𝑥 )