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 <-> A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) )

Proof

Step	Hyp	Ref	Expression
1		dfeldisj5	|- ( ElDisj A <-> A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = (/) ) )
2		orcom	|- ( ( u = v \/ ( u i^i v ) = (/) ) <-> ( ( u i^i v ) = (/) \/ u = v ) )
3		neor	|- ( ( ( u i^i v ) = (/) \/ u = v ) <-> ( ( u i^i v ) =/= (/) -> u = v ) )
4	2 3	bitri	|- ( ( u = v \/ ( u i^i v ) = (/) ) <-> ( ( u i^i v ) =/= (/) -> u = v ) )
5	4	2ralbii	|- ( A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = (/) ) <-> A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) )
6	1 5	bitri	|- ( ElDisj A <-> A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) )