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 x * y ran R x R y x * y x R y

Proof

Step Hyp Ref Expression
1 df-rmo * y ran R x R y * y y ran R x R y
2 cnvresrn R -1 ran R = R -1
3 2 breqi y R -1 ran R x y R -1 x
4 brres x V y R -1 ran R x y ran R y R -1 x
5 4 elv y R -1 ran R x y ran R y R -1 x
6 brcnvg y V x V y R -1 x x R y
7 6 el2v y R -1 x x R y
8 7 anbi2i y ran R y R -1 x y ran R x R y
9 5 8 bitri y R -1 ran R x y ran R x R y
10 3 9 7 3bitr3i y ran R x R y x R y
11 10 mobii * y y ran R x R y * y x R y
12 1 11 bitri * y ran R x R y * y x R y
13 12 albii x * y ran R x R y x * y x R y