Metamath Proof Explorer

Theorem elpwun

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

Ref Expression
Hypothesis eldifpw.1 ⊢C∈V
Assertion elpwun ⊢A∈𝒫B∪C↔A∖C∈𝒫B

Proof

Step Hyp Ref Expression
1 eldifpw.1 ⊢C∈V
2 elex ⊢A∈𝒫B∪C→A∈V
3 elex ⊢A∖C∈𝒫B→A∖C∈V
4 difex2 ⊢C∈V→A∈V↔A∖C∈V
5 1 4 ax-mp ⊢A∈V↔A∖C∈V
6 3 5 sylibr ⊢A∖C∈𝒫B→A∈V
7 elpwg ⊢A∈V→A∈𝒫B∪C↔A⊆B∪C
8 uncom ⊢B∪C=C∪B
9 8 sseq2i ⊢A⊆B∪C↔A⊆C∪B
10 ssundif ⊢A⊆C∪B↔A∖C⊆B
11 9 10 bitri ⊢A⊆B∪C↔A∖C⊆B
12 difexg ⊢A∈V→A∖C∈V
13 elpwg ⊢A∖C∈V→A∖C∈𝒫B↔A∖C⊆B
14 12 13 syl ⊢A∈V→A∖C∈𝒫B↔A∖C⊆B
15 11 14 bitr4id ⊢A∈V→A⊆B∪C↔A∖C∈𝒫B
16 7 15 bitrd ⊢A∈V→A∈𝒫B∪C↔A∖C∈𝒫B
17 2 6 16 pm5.21nii ⊢A∈𝒫B∪C↔A∖C∈𝒫B