Theorem alrmomorn

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

	Ref	Expression
Assertion	alrmomorn	|- ( A. x E* y e. ran R x R y <-> A. x E* y x R y )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	|- ( E* y e. ran R x R y <-> E* y ( y e. ran R /\ x R y ) )
2		cnvresrn	|- ( `' R |` ran R ) = `' R
3	2	breqi	|- ( y ( `' R |` ran R ) x <-> y `' R x )
4		brres	|- ( x e. _V -> ( y ( `' R |` ran R ) x <-> ( y e. ran R /\ y `' R x ) ) )
5	4	elv	|- ( y ( `' R |` ran R ) x <-> ( y e. ran R /\ y `' R x ) )
6		brcnvg	|- ( ( y e. _V /\ x e. _V ) -> ( y `' R x <-> x R y ) )
7	6	el2v	|- ( y `' R x <-> x R y )
8	7	anbi2i	|- ( ( y e. ran R /\ y `' R x ) <-> ( y e. ran R /\ x R y ) )
9	5 8	bitri	|- ( y ( `' R |` ran R ) x <-> ( y e. ran R /\ x R y ) )
10	3 9 7	3bitr3i	|- ( ( y e. ran R /\ x R y ) <-> x R y )
11	10	mobii	|- ( E* y ( y e. ran R /\ x R y ) <-> E* y x R y )
12	1 11	bitri	|- ( E* y e. ran R x R y <-> E* y x R y )
13	12	albii	|- ( A. x E* y e. ran R x R y <-> A. x E* y x R y )