Metamath Proof Explorer


Theorem inecmo3

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

Ref Expression
Assertion inecmo3 u dom R v dom R u = v u R v R = Rel R x * u u R x Rel R

Proof

Step Hyp Ref Expression
1 inecmo2 u dom R v dom R u = v u R v R = Rel R x * u dom R u R x Rel R
2 alrmomodm Rel R x * u dom R u R x x * u u R x
3 2 pm5.32ri x * u dom R u R x Rel R x * u u R x Rel R
4 1 3 bitri u dom R v dom R u = v u R v R = Rel R x * u u R x Rel R