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

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