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 ∈ A x ∈ B
4 2 3 bitrdi ⊢ A ∈ 𝒫 B ∪ C → A ∈ 𝒫 B ↔ ∀ x ∈ A x ∈ B
5 4 notbid ⊢ A ∈ 𝒫 B ∪ C → ¬ A ∈ 𝒫 B ↔ ¬ ∀ x ∈ A x ∈ B
6 5 biimpa ⊢ A ∈ 𝒫 B ∪ C ∧ ¬ A ∈ 𝒫 B → ¬ ∀ x ∈ A x ∈ B
7 rexnal ⊢ ∃ x ∈ A ¬ x ∈ B ↔ ¬ ∀ x ∈ A x ∈ 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