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

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

Proof

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