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 x * u dom R u R x x * u u R x

Proof

Step Hyp Ref Expression
1 df-rmo * u dom R u R x * u u dom R u R x
2 brres x V u R dom R x u dom R u R x
3 2 elv u R dom R x u 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 dom R u R x u R x
7 6 mobidv Rel R * u u dom R u R x * u u R x
8 1 7 syl5bb Rel R * u dom R u R x * u u R x
9 8 albidv Rel R x * u dom R u R x x * u u R x