Metamath Proof Explorer

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 ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R ↔ ∀ x ∃* u ∈ A u R x ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 id ⊢ u = v → u = v
2 1 inecmo ⊢ Rel ⁡ R → ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ x ∃* u ∈ A u R x
3 2 pm5.32ri ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R ↔ ∀ x ∃* u ∈ A u R x ∧ Rel ⁡ R