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 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 bitrid 
 |-  ( 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 ) )