Metamath Proof Explorer

Theorem eldisjlem19

Description: Special case of disjlem19 (together with membpartlem19 , this is former prtlem19 ). (Contributed by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion eldisjlem19 
|- ( B e. V -> ( ElDisj A -> ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> u = [ B ] ~ A ) ) )

Proof

Step Hyp Ref Expression
1 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
2 disjlem19 
 |-  ( B e. V -> ( Disj ( `' _E |` A ) -> ( ( u e. dom ( `' _E |` A ) /\ B e. [ u ] ( `' _E |` A ) ) -> [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) ) ) )
3 1 2 biimtrid 
 |-  ( B e. V -> ( ElDisj A -> ( ( u e. dom ( `' _E |` A ) /\ B e. [ u ] ( `' _E |` A ) ) -> [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) ) ) )
4 3 imp 
 |-  ( ( B e. V /\ ElDisj A ) -> ( ( u e. dom ( `' _E |` A ) /\ B e. [ u ] ( `' _E |` A ) ) -> [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) ) )
5 4 expdimp 
 |-  ( ( ( B e. V /\ ElDisj A ) /\ u e. dom ( `' _E |` A ) ) -> ( B e. [ u ] ( `' _E |` A ) -> [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) ) )
6 eccnvepres3 
 |-  ( u e. dom ( `' _E |` A ) -> [ u ] ( `' _E |` A ) = u )
7 6 eleq2d 
 |-  ( u e. dom ( `' _E |` A ) -> ( B e. [ u ] ( `' _E |` A ) <-> B e. u ) )
8 6 eqeq1d 
 |-  ( u e. dom ( `' _E |` A ) -> ( [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) <-> u = [ B ] ,~ ( `' _E |` A ) ) )
9 7 8 imbi12d 
 |-  ( u e. dom ( `' _E |` A ) -> ( ( B e. [ u ] ( `' _E |` A ) -> [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) ) <-> ( B e. u -> u = [ B ] ,~ ( `' _E |` A ) ) ) )
10 9 adantl 
 |-  ( ( ( B e. V /\ ElDisj A ) /\ u e. dom ( `' _E |` A ) ) -> ( ( B e. [ u ] ( `' _E |` A ) -> [ u ] ( `' _E |` A ) = [ B ] ,~ ( `' _E |` A ) ) <-> ( B e. u -> u = [ B ] ,~ ( `' _E |` A ) ) ) )
11 5 10 mpbid 
 |-  ( ( ( B e. V /\ ElDisj A ) /\ u e. dom ( `' _E |` A ) ) -> ( B e. u -> u = [ B ] ,~ ( `' _E |` A ) ) )
12 df-coels 
 |-  ~ A = ,~ ( `' _E |` A )
13 12 eceq2i 
 |-  [ B ] ~ A = [ B ] ,~ ( `' _E |` A )
14 13 eqeq2i 
 |-  ( u = [ B ] ~ A <-> u = [ B ] ,~ ( `' _E |` A ) )
15 11 14 imbitrrdi 
 |-  ( ( ( B e. V /\ ElDisj A ) /\ u e. dom ( `' _E |` A ) ) -> ( B e. u -> u = [ B ] ~ A ) )
16 15 expimpd 
 |-  ( ( B e. V /\ ElDisj A ) -> ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> u = [ B ] ~ A ) )
17 16 ex 
 |-  ( B e. V -> ( ElDisj A -> ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> u = [ B ] ~ A ) ) )