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

Metamath Proof Explorer

Theorem dfeldisj4

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj4 
|- ( ElDisj A <-> A. x E* u e. A x e. u )

Proof

Step Hyp Ref Expression
1 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
2 relres 
 |-  Rel ( `' _E |` A )
3 dfdisjALTV4 
 |-  ( Disj ( `' _E |` A ) <-> ( A. x E* u u ( `' _E |` A ) x /\ Rel ( `' _E |` A ) ) )
4 2 3 mpbiran2 
 |-  ( Disj ( `' _E |` A ) <-> A. x E* u u ( `' _E |` A ) x )
5 brcnvepres 
 |-  ( ( u e. _V /\ x e. _V ) -> ( u ( `' _E |` A ) x <-> ( u e. A /\ x e. u ) ) )
6 5 el2v 
 |-  ( u ( `' _E |` A ) x <-> ( u e. A /\ x e. u ) )
7 6 mobii 
 |-  ( E* u u ( `' _E |` A ) x <-> E* u ( u e. A /\ x e. u ) )
8 df-rmo 
 |-  ( E* u e. A x e. u <-> E* u ( u e. A /\ x e. u ) )
9 7 8 bitr4i 
 |-  ( E* u u ( `' _E |` A ) x <-> E* u e. A x e. u )
10 9 albii 
 |-  ( A. x E* u u ( `' _E |` A ) x <-> A. x E* u e. A x e. u )
11 1 4 10 3bitri 
 |-  ( ElDisj A <-> A. x E* u e. A x e. u )