Metamath Proof Explorer

Theorem membpartlem19

Description: Together with disjlem19 , this is former prtlem19 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion membpartlem19 
|- ( B e. V -> ( MembPart A -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) )

Proof

Step Hyp Ref Expression
1 dfmembpart2 
 |-  ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) )
2 n0el2 
 |-  ( -. (/) e. A <-> dom ( `' _E |` A ) = A )
3 2 biimpi 
 |-  ( -. (/) e. A -> dom ( `' _E |` A ) = A )
4 3 ad2antll 
 |-  ( ( B e. V /\ ( ElDisj A /\ -. (/) e. A ) ) -> dom ( `' _E |` A ) = A )
5 4 eleq2d 
 |-  ( ( B e. V /\ ( ElDisj A /\ -. (/) e. A ) ) -> ( u e. dom ( `' _E |` A ) <-> u e. A ) )
6 eldisjlem19 
 |-  ( B e. V -> ( ElDisj A -> ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> u = [ B ] ~ A ) ) )
7 6 adantrd 
 |-  ( B e. V -> ( ( ElDisj A /\ -. (/) e. A ) -> ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> u = [ B ] ~ A ) ) )
8 7 imp 
 |-  ( ( B e. V /\ ( ElDisj A /\ -. (/) e. A ) ) -> ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> u = [ B ] ~ A ) )
9 8 expd 
 |-  ( ( B e. V /\ ( ElDisj A /\ -. (/) e. A ) ) -> ( u e. dom ( `' _E |` A ) -> ( B e. u -> u = [ B ] ~ A ) ) )
10 5 9 sylbird 
 |-  ( ( B e. V /\ ( ElDisj A /\ -. (/) e. A ) ) -> ( u e. A -> ( B e. u -> u = [ B ] ~ A ) ) )
11 1 10 sylan2b 
 |-  ( ( B e. V /\ MembPart A ) -> ( u e. A -> ( B e. u -> u = [ B ] ~ A ) ) )
12 11 impd 
 |-  ( ( B e. V /\ MembPart A ) -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) )
13 12 ex 
 |-  ( B e. V -> ( MembPart A -> ( ( u e. A /\ B e. u ) -> u = [ B ] ~ A ) ) )