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	$$⊢ElDisjA\leftrightarrow \forall u\in A\forall v\in A\left(u\cap v\ne \varnothing \to u=v\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfeldisj5	$$⊢ElDisjA\leftrightarrow \forall u\in A\forall v\in A\left(u=v\vee u\cap v=\varnothing \right)$$
2		orcom	$$⊢\left(u=v\vee u\cap v=\varnothing \right)\leftrightarrow \left(u\cap v=\varnothing \vee u=v\right)$$
3		neor	$$⊢\left(u\cap v=\varnothing \vee u=v\right)\leftrightarrow \left(u\cap v\ne \varnothing \to u=v\right)$$
4	2 3	bitri	$$⊢\left(u=v\vee u\cap v=\varnothing \right)\leftrightarrow \left(u\cap v\ne \varnothing \to u=v\right)$$
5	4	2ralbii	$$⊢\forall u\in A\forall v\in A\left(u=v\vee u\cap v=\varnothing \right)\leftrightarrow \forall u\in A\forall v\in A\left(u\cap v\ne \varnothing \to u=v\right)$$
6	1 5	bitri	$$⊢ElDisjA\leftrightarrow \forall u\in A\forall v\in A\left(u\cap v\ne \varnothing \to u=v\right)$$