Theorem elpwun

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

	Ref	Expression
Hypothesis	eldifpw.1	⊢ 𝐶 ∈ V
Assertion	elpwun	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∖ 𝐶 ) ∈ 𝒫 𝐵 )

Proof

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