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 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝑢 ∩ 𝑣 ) ≠ ∅ → 𝑢 = 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		dfeldisj5	⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
2		orcom	⊢ ( ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( ( 𝑢 ∩ 𝑣 ) = ∅ ∨ 𝑢 = 𝑣 ) )
3		neor	⊢ ( ( ( 𝑢 ∩ 𝑣 ) = ∅ ∨ 𝑢 = 𝑣 ) ↔ ( ( 𝑢 ∩ 𝑣 ) ≠ ∅ → 𝑢 = 𝑣 ) )
4	2 3	bitri	⊢ ( ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( ( 𝑢 ∩ 𝑣 ) ≠ ∅ → 𝑢 = 𝑣 ) )
5	4	2ralbii	⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝑢 ∩ 𝑣 ) ≠ ∅ → 𝑢 = 𝑣 ) )
6	1 5	bitri	⊢ ( ElDisj 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( ( 𝑢 ∩ 𝑣 ) ≠ ∅ → 𝑢 = 𝑣 ) )