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	syl5ibr	|- ( 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 ) )