Metamath Proof Explorer

Theorem elpwunsn

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

Ref Expression
Assertion elpwunsn ⊢A∈𝒫B∪C∖𝒫B→C∈A

Proof

Step Hyp Ref Expression
1 eldif ⊢A∈𝒫B∪C∖𝒫B↔A∈𝒫B∪C∧¬A∈𝒫B
2 elpwg ⊢A∈𝒫B∪C→A∈𝒫B↔A⊆B
3 dfss3 ⊢A⊆B↔∀x∈Ax∈B
4 2 3 bitrdi ⊢A∈𝒫B∪C→A∈𝒫B↔∀x∈Ax∈B
5 4 notbid ⊢A∈𝒫B∪C→¬A∈𝒫B↔¬∀x∈Ax∈B
6 5 biimpa ⊢A∈𝒫B∪C∧¬A∈𝒫B→¬∀x∈Ax∈B
7 rexnal ⊢∃x∈A¬x∈B↔¬∀x∈Ax∈B
8 6 7 sylibr ⊢A∈𝒫B∪C∧¬A∈𝒫B→∃x∈A¬x∈B
9 elpwi ⊢A∈𝒫B∪C→A⊆B∪C
10 ssel ⊢A⊆B∪C→x∈A→x∈B∪C
11 elun ⊢x∈B∪C↔x∈B∨x∈C
12 elsni ⊢x∈C→x=C
13 12 orim2i ⊢x∈B∨x∈C→x∈B∨x=C
14 13 ord ⊢x∈B∨x∈C→¬x∈B→x=C
15 11 14 sylbi ⊢x∈B∪C→¬x∈B→x=C
16 15 imim2i ⊢x∈A→x∈B∪C→x∈A→¬x∈B→x=C
17 16 impd ⊢x∈A→x∈B∪C→x∈A∧¬x∈B→x=C
18 9 10 17 3syl ⊢A∈𝒫B∪C→x∈A∧¬x∈B→x=C
19 eleq1 ⊢x=C→x∈A↔C∈A
20 19 biimpd ⊢x=C→x∈A→C∈A
21 18 20 syl6 ⊢A∈𝒫B∪C→x∈A∧¬x∈B→x∈A→C∈A
22 21 expd ⊢A∈𝒫B∪C→x∈A→¬x∈B→x∈A→C∈A
23 22 com4r ⊢x∈A→A∈𝒫B∪C→x∈A→¬x∈B→C∈A
24 23 pm2.43b ⊢A∈𝒫B∪C→x∈A→¬x∈B→C∈A
25 24 rexlimdv ⊢A∈𝒫B∪C→∃x∈A¬x∈B→C∈A
26 25 imp ⊢A∈𝒫B∪C∧∃x∈A¬x∈B→C∈A
27 8 26 syldan ⊢A∈𝒫B∪C∧¬A∈𝒫B→C∈A
28 1 27 sylbi ⊢A∈𝒫B∪C∖𝒫B→C∈A