Theorem elpwun

Description: Membership in the power class of a union. (Contributed by NM, 26-Mar-2007)

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

Proof

Step	Hyp	Ref	Expression
1		eldifpw.1	|- C e. _V
2		elex	|- ( A e. ~P ( B u. C ) -> A e. _V )
3		elex	|- ( ( A \ C ) e. ~P B -> ( A \ C ) e. _V )
4		difex2	|- ( C e. _V -> ( A e. _V <-> ( A \ C ) e. _V ) )
5	1 4	ax-mp	|- ( A e. _V <-> ( A \ C ) e. _V )
6	3 5	sylibr	|- ( ( A \ C ) e. ~P B -> A e. _V )
7		elpwg	|- ( A e. _V -> ( A e. ~P ( B u. C ) <-> A C_ ( B u. C ) ) )
8		uncom	|- ( B u. C ) = ( C u. B )
9	8	sseq2i	|- ( A C_ ( B u. C ) <-> A C_ ( C u. B ) )
10		ssundif	|- ( A C_ ( C u. B ) <-> ( A \ C ) C_ B )
11	9 10	bitri	|- ( A C_ ( B u. C ) <-> ( A \ C ) C_ B )
12		difexg	|- ( A e. _V -> ( A \ C ) e. _V )
13		elpwg	|- ( ( A \ C ) e. _V -> ( ( A \ C ) e. ~P B <-> ( A \ C ) C_ B ) )
14	12 13	syl	|- ( A e. _V -> ( ( A \ C ) e. ~P B <-> ( A \ C ) C_ B ) )
15	11 14	bitr4id	|- ( A e. _V -> ( A C_ ( B u. C ) <-> ( A \ C ) e. ~P B ) )
16	7 15	bitrd	|- ( A e. _V -> ( A e. ~P ( B u. C ) <-> ( A \ C ) e. ~P B ) )
17	2 6 16	pm5.21nii	|- ( A e. ~P ( B u. C ) <-> ( A \ C ) e. ~P B )