This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfeldisj5a

Description: Alternate definition of the disjoint elementhood predicate. Members of A are pairwise disjoint: if two members overlap, they are equal. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj5a ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A u ∩ v ≠ ∅ → u = v

Proof

Step Hyp Ref Expression
1 dfeldisj5 ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u ∩ v = ∅
2 orcom ⊢ u = v ∨ u ∩ v = ∅ ↔ u ∩ v = ∅ ∨ u = v
3 neor ⊢ u ∩ v = ∅ ∨ u = v ↔ u ∩ v ≠ ∅ → u = v
4 2 3 bitri ⊢ u = v ∨ u ∩ v = ∅ ↔ u ∩ v ≠ ∅ → u = v
5 4 2ralbii ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u ∩ v = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u ∩ v ≠ ∅ → u = v
6 1 5 bitri ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A u ∩ v ≠ ∅ → u = v