Theorem ralmo

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

	Ref	Expression
Assertion	ralmo	⊢ ( ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∈ ran 𝑅 ∃* 𝑢 𝑢 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		brelrng	⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ∧ 𝑢 𝑅 𝑥 ) → 𝑥 ∈ ran 𝑅 )
2	1	el3v12	⊢ ( 𝑢 𝑅 𝑥 → 𝑥 ∈ ran 𝑅 )
3	2	pm4.71ri	⊢ ( 𝑢 𝑅 𝑥 ↔ ( 𝑥 ∈ ran 𝑅 ∧ 𝑢 𝑅 𝑥 ) )
4	3	mobii	⊢ ( ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∃* 𝑢 ( 𝑥 ∈ ran 𝑅 ∧ 𝑢 𝑅 𝑥 ) )
5		moanimv	⊢ ( ∃* 𝑢 ( 𝑥 ∈ ran 𝑅 ∧ 𝑢 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ran 𝑅 → ∃* 𝑢 𝑢 𝑅 𝑥 ) )
6	4 5	bitri	⊢ ( ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ( 𝑥 ∈ ran 𝑅 → ∃* 𝑢 𝑢 𝑅 𝑥 ) )
7	6	albii	⊢ ( ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ ran 𝑅 → ∃* 𝑢 𝑢 𝑅 𝑥 ) )
8		df-ral	⊢ ( ∀ 𝑥 ∈ ran 𝑅 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ ran 𝑅 → ∃* 𝑢 𝑢 𝑅 𝑥 ) )
9	7 8	bitr4i	⊢ ( ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∈ ran 𝑅 ∃* 𝑢 𝑢 𝑅 𝑥 )