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

Metamath Proof Explorer

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 )