Metamath Proof Explorer

Theorem ineccnvmo2

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

Ref Expression
Assertion ineccnvmo2 ⊢ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ↔ ∀ u ∃* x u F x

Proof

Step Hyp Ref Expression
1 ineccnvmo ⊢ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ↔ ∀ u ∃* x ∈ ran ⁡ F u F x
2 alrmomorn ⊢ ∀ u ∃* x ∈ ran ⁡ F u F x ↔ ∀ u ∃* x u F x
3 1 2 bitri ⊢ ∀ x ∈ ran ⁡ F ∀ y ∈ ran ⁡ F x = y ∨ x F -1 ∩ y F -1 = ∅ ↔ ∀ u ∃* x u F x