Theorem elpwunsn

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

	Ref	Expression
Assertion	elpwunsn	|- ( A e. ( ~P ( B u. { C } ) \ ~P B ) -> C e. A )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( ~P ( B u. { C } ) \ ~P B ) <-> ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) )
2		elpwg	|- ( A e. ~P ( B u. { C } ) -> ( A e. ~P B <-> A C_ B ) )
3		dfss3	|- ( A C_ B <-> A. x e. A x e. B )
4	2 3	bitrdi	|- ( A e. ~P ( B u. { C } ) -> ( A e. ~P B <-> A. x e. A x e. B ) )
5	4	notbid	|- ( A e. ~P ( B u. { C } ) -> ( -. A e. ~P B <-> -. A. x e. A x e. B ) )
6	5	biimpa	|- ( ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) -> -. A. x e. A x e. B )
7		rexnal	|- ( E. x e. A -. x e. B <-> -. A. x e. A x e. B )
8	6 7	sylibr	|- ( ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) -> E. x e. A -. x e. B )
9		elpwi	|- ( A e. ~P ( B u. { C } ) -> A C_ ( B u. { C } ) )
10		ssel	|- ( A C_ ( B u. { C } ) -> ( x e. A -> x e. ( B u. { C } ) ) )
11		elun	|- ( x e. ( B u. { C } ) <-> ( x e. B \/ x e. { C } ) )
12		elsni	|- ( x e. { C } -> x = C )
13	12	orim2i	|- ( ( x e. B \/ x e. { C } ) -> ( x e. B \/ x = C ) )
14	13	ord	|- ( ( x e. B \/ x e. { C } ) -> ( -. x e. B -> x = C ) )
15	11 14	sylbi	|- ( x e. ( B u. { C } ) -> ( -. x e. B -> x = C ) )
16	15	imim2i	|- ( ( x e. A -> x e. ( B u. { C } ) ) -> ( x e. A -> ( -. x e. B -> x = C ) ) )
17	16	impd	|- ( ( x e. A -> x e. ( B u. { C } ) ) -> ( ( x e. A /\ -. x e. B ) -> x = C ) )
18	9 10 17	3syl	|- ( A e. ~P ( B u. { C } ) -> ( ( x e. A /\ -. x e. B ) -> x = C ) )
19		eleq1	|- ( x = C -> ( x e. A <-> C e. A ) )
20	19	biimpd	|- ( x = C -> ( x e. A -> C e. A ) )
21	18 20	syl6	|- ( A e. ~P ( B u. { C } ) -> ( ( x e. A /\ -. x e. B ) -> ( x e. A -> C e. A ) ) )
22	21	expd	|- ( A e. ~P ( B u. { C } ) -> ( x e. A -> ( -. x e. B -> ( x e. A -> C e. A ) ) ) )
23	22	com4r	|- ( x e. A -> ( A e. ~P ( B u. { C } ) -> ( x e. A -> ( -. x e. B -> C e. A ) ) ) )
24	23	pm2.43b	|- ( A e. ~P ( B u. { C } ) -> ( x e. A -> ( -. x e. B -> C e. A ) ) )
25	24	rexlimdv	|- ( A e. ~P ( B u. { C } ) -> ( E. x e. A -. x e. B -> C e. A ) )
26	25	imp	|- ( ( A e. ~P ( B u. { C } ) /\ E. x e. A -. x e. B ) -> C e. A )
27	8 26	syldan	|- ( ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) -> C e. A )
28	1 27	sylbi	|- ( A e. ( ~P ( B u. { C } ) \ ~P B ) -> C e. A )