Theorem inecmo2

Description: Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018) (Revised by Peter Mazsa, 2-Sep-2021)

	Ref	Expression
Assertion	inecmo2	$$⊢\left(\forall u\in A\forall v\in A\left(u=v\vee \left[u\right]R\cap \left[v\right]R=\varnothing \right)\wedge \mathrm{Rel}R\right)\leftrightarrow \left(\forall x{\exists }^{*}u\in AuRx\wedge \mathrm{Rel}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢u=v\to u=v$$
2	1	inecmo	$$⊢\mathrm{Rel}R\to \left(\forall u\in A\forall v\in A\left(u=v\vee \left[u\right]R\cap \left[v\right]R=\varnothing \right)\leftrightarrow \forall x{\exists }^{*}u\in AuRx\right)$$
3	2	pm5.32ri	$$⊢\left(\forall u\in A\forall v\in A\left(u=v\vee \left[u\right]R\cap \left[v\right]R=\varnothing \right)\wedge \mathrm{Rel}R\right)\leftrightarrow \left(\forall x{\exists }^{*}u\in AuRx\wedge \mathrm{Rel}R\right)$$