Metamath Proof Explorer

Theorem alrmomodm

Description: Equivalence of an "at most one" and an "at most one" restricted to the domain inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion alrmomodm ⊢ Rel ⁡ R → ∀ x ∃* u ∈ dom ⁡ R u R x ↔ ∀ x ∃* u u R x

Proof

Step Hyp Ref Expression
1 df-rmo ⊢ ∃* u ∈ dom ⁡ R u R x ↔ ∃* u u ∈ dom ⁡ R ∧ u R x
2 brres ⊢ x ∈ V → u R ↾ dom ⁡ R x ↔ u ∈ dom ⁡ R ∧ u R x
3 2 elv ⊢ u R ↾ dom ⁡ R x ↔ u ∈ dom ⁡ R ∧ u R x
4 resdm ⊢ Rel ⁡ R → R ↾ dom ⁡ R = R
5 4 breqd ⊢ Rel ⁡ R → u R ↾ dom ⁡ R x ↔ u R x
6 3 5 bitr3id ⊢ Rel ⁡ R → u ∈ dom ⁡ R ∧ u R x ↔ u R x
7 6 mobidv ⊢ Rel ⁡ R → ∃* u u ∈ dom ⁡ R ∧ u R x ↔ ∃* u u R x
8 1 7 bitrid ⊢ Rel ⁡ R → ∃* u ∈ dom ⁡ R u R x ↔ ∃* u u R x
9 8 albidv ⊢ Rel ⁡ R → ∀ x ∃* u ∈ dom ⁡ R u R x ↔ ∀ x ∃* u u R x