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

Metamath Proof Explorer

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 ⊢ ∀ x ∈ ran ⁡ R ∃* u u R x ↔ ∀ x ∈ ran ⁡ R ∃! u u R x

Proof

Step Hyp Ref Expression
1 dfrn2 ⊢ ran ⁡ R = x | ∃ u u R x
2 1 eqabri ⊢ x ∈ ran ⁡ R ↔ ∃ u u R x
3 2 biimpi ⊢ x ∈ ran ⁡ R → ∃ u u R x
4 3 biantrurd ⊢ x ∈ ran ⁡ R → ∃* u u R x ↔ ∃ u u R x ∧ ∃* u u R x
5 4 ralbiia ⊢ ∀ x ∈ ran ⁡ R ∃* u u R x ↔ ∀ x ∈ ran ⁡ R ∃ u u R x ∧ ∃* u u R x
6 df-eu ⊢ ∃! u u R x ↔ ∃ u u R x ∧ ∃* u u R x
7 6 ralbii ⊢ ∀ x ∈ ran ⁡ R ∃! u u R x ↔ ∀ x ∈ ran ⁡ R ∃ u u R x ∧ ∃* u u R x
8 5 7 bitr4i ⊢ ∀ x ∈ ran ⁡ R ∃* u u R x ↔ ∀ x ∈ ran ⁡ R ∃! u u R x