This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐶 ∈ 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 ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∖ 𝐶 ) ∈ 𝒫 𝐵 )