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 -> ( A. x E* u e. dom R u R x <-> A. x E* u u R x ) )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	|- ( E* u e. dom R u R x <-> E* u ( u e. dom R /\ u R x ) )
2		brres	|- ( x e. _V -> ( u ( R |` dom R ) x <-> ( u e. dom R /\ u R x ) ) )
3	2	elv	|- ( u ( R |` dom R ) x <-> ( u e. 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 e. dom R /\ u R x ) <-> u R x ) )
7	6	mobidv	|- ( Rel R -> ( E* u ( u e. dom R /\ u R x ) <-> E* u u R x ) )
8	1 7	syl5bb	|- ( Rel R -> ( E* u e. dom R u R x <-> E* u u R x ) )
9	8	albidv	|- ( Rel R -> ( A. x E* u e. dom R u R x <-> A. x E* u u R x ) )