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	syl5bb	⊢ ( Rel 𝑅 → ( ∃* 𝑢 ∈ dom 𝑅 𝑢 𝑅 𝑥 ↔ ∃* 𝑢 𝑢 𝑅 𝑥 ) )
9	8	albidv	⊢ ( Rel 𝑅 → ( ∀ 𝑥 ∃* 𝑢 ∈ dom 𝑅 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∃* 𝑢 𝑢 𝑅 𝑥 ) )