Metamath Proof Explorer

Theorem dfeldisj3

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

Ref Expression
Assertion dfeldisj3 
|- ( ElDisj A <-> A. u e. A A. v e. A A. x e. ( u i^i v ) u = v )

Proof

Step Hyp Ref Expression
1 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
2 relres 
 |-  Rel ( `' _E |` A )
3 dfdisjALTV3 
 |-  ( Disj ( `' _E |` A ) <-> ( A. u A. v A. x ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) -> u = v ) /\ Rel ( `' _E |` A ) ) )
4 2 3 mpbiran2 
 |-  ( Disj ( `' _E |` A ) <-> A. u A. v A. x ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) -> u = v ) )
5 an4 
 |-  ( ( ( u e. A /\ x e. u ) /\ ( v e. A /\ x e. v ) ) <-> ( ( u e. A /\ v e. A ) /\ ( x e. u /\ x e. v ) ) )
6 brcnvepres 
 |-  ( ( u e. _V /\ x e. _V ) -> ( u ( `' _E |` A ) x <-> ( u e. A /\ x e. u ) ) )
7 6 el2v 
 |-  ( u ( `' _E |` A ) x <-> ( u e. A /\ x e. u ) )
8 brcnvepres 
 |-  ( ( v e. _V /\ x e. _V ) -> ( v ( `' _E |` A ) x <-> ( v e. A /\ x e. v ) ) )
9 8 el2v 
 |-  ( v ( `' _E |` A ) x <-> ( v e. A /\ x e. v ) )
10 7 9 anbi12i 
 |-  ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) <-> ( ( u e. A /\ x e. u ) /\ ( v e. A /\ x e. v ) ) )
11 elin 
 |-  ( x e. ( u i^i v ) <-> ( x e. u /\ x e. v ) )
12 11 anbi2i 
 |-  ( ( ( u e. A /\ v e. A ) /\ x e. ( u i^i v ) ) <-> ( ( u e. A /\ v e. A ) /\ ( x e. u /\ x e. v ) ) )
13 5 10 12 3bitr4i 
 |-  ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) <-> ( ( u e. A /\ v e. A ) /\ x e. ( u i^i v ) ) )
14 df-3an 
 |-  ( ( u e. A /\ v e. A /\ x e. ( u i^i v ) ) <-> ( ( u e. A /\ v e. A ) /\ x e. ( u i^i v ) ) )
15 13 14 bitr4i 
 |-  ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) <-> ( u e. A /\ v e. A /\ x e. ( u i^i v ) ) )
16 15 imbi1i 
 |-  ( ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) -> u = v ) <-> ( ( u e. A /\ v e. A /\ x e. ( u i^i v ) ) -> u = v ) )
17 16 3albii 
 |-  ( A. u A. v A. x ( ( u ( `' _E |` A ) x /\ v ( `' _E |` A ) x ) -> u = v ) <-> A. u A. v A. x ( ( u e. A /\ v e. A /\ x e. ( u i^i v ) ) -> u = v ) )
18 1 4 17 3bitri 
 |-  ( ElDisj A <-> A. u A. v A. x ( ( u e. A /\ v e. A /\ x e. ( u i^i v ) ) -> u = v ) )
19 r3al 
 |-  ( A. u e. A A. v e. A A. x e. ( u i^i v ) u = v <-> A. u A. v A. x ( ( u e. A /\ v e. A /\ x e. ( u i^i v ) ) -> u = v ) )
20 18 19 bitr4i 
 |-  ( ElDisj A <-> A. u e. A A. v e. A A. x e. ( u i^i v ) u = v )