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 <-> 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 ) )