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

Metamath Proof Explorer

Theorem eldifpw

Description: Membership in a power class difference. (Contributed by NM, 25-Mar-2007)

Ref Expression
Hypothesis eldifpw.1 
|- C e. _V
Assertion eldifpw 
|- ( ( A e. ~P B /\ -. C C_ B ) -> ( A u. C ) e. ( ~P ( B u. C ) \ ~P B ) )

Proof

Step Hyp Ref Expression
1 eldifpw.1 
 |-  C e. _V
2 elpwi 
 |-  ( A e. ~P B -> A C_ B )
3 unss1 
 |-  ( A C_ B -> ( A u. C ) C_ ( B u. C ) )
4 unexg 
 |-  ( ( A e. ~P B /\ C e. _V ) -> ( A u. C ) e. _V )
5 1 4 mpan2 
 |-  ( A e. ~P B -> ( A u. C ) e. _V )
6 elpwg 
 |-  ( ( A u. C ) e. _V -> ( ( A u. C ) e. ~P ( B u. C ) <-> ( A u. C ) C_ ( B u. C ) ) )
7 5 6 syl 
 |-  ( A e. ~P B -> ( ( A u. C ) e. ~P ( B u. C ) <-> ( A u. C ) C_ ( B u. C ) ) )
8 3 7 imbitrrid 
 |-  ( A e. ~P B -> ( A C_ B -> ( A u. C ) e. ~P ( B u. C ) ) )
9 2 8 mpd 
 |-  ( A e. ~P B -> ( A u. C ) e. ~P ( B u. C ) )
10 elpwi 
 |-  ( ( A u. C ) e. ~P B -> ( A u. C ) C_ B )
11 10 unssbd 
 |-  ( ( A u. C ) e. ~P B -> C C_ B )
12 11 con3i 
 |-  ( -. C C_ B -> -. ( A u. C ) e. ~P B )
13 9 12 anim12i 
 |-  ( ( A e. ~P B /\ -. C C_ B ) -> ( ( A u. C ) e. ~P ( B u. C ) /\ -. ( A u. C ) e. ~P B ) )
14 eldif 
 |-  ( ( A u. C ) e. ( ~P ( B u. C ) \ ~P B ) <-> ( ( A u. C ) e. ~P ( B u. C ) /\ -. ( A u. C ) e. ~P B ) )
15 13 14 sylibr 
 |-  ( ( A e. ~P B /\ -. C C_ B ) -> ( A u. C ) e. ( ~P ( B u. C ) \ ~P B ) )