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 
|- C e. _V
Assertion elpwun 
|- ( A e. ~P ( B u. C ) <-> ( A \ C ) e. ~P B )

Proof

Step Hyp Ref Expression
1 eldifpw.1 
 |-  C e. _V
2 elex 
 |-  ( A e. ~P ( B u. C ) -> A e. _V )
3 elex 
 |-  ( ( A \ C ) e. ~P B -> ( A \ C ) e. _V )
4 difex2 
 |-  ( C e. _V -> ( A e. _V <-> ( A \ C ) e. _V ) )
5 1 4 ax-mp 
 |-  ( A e. _V <-> ( A \ C ) e. _V )
6 3 5 sylibr 
 |-  ( ( A \ C ) e. ~P B -> A e. _V )
7 elpwg 
 |-  ( A e. _V -> ( A e. ~P ( B u. C ) <-> A C_ ( B u. C ) ) )
8 uncom 
 |-  ( B u. C ) = ( C u. B )
9 8 sseq2i 
 |-  ( A C_ ( B u. C ) <-> A C_ ( C u. B ) )
10 ssundif 
 |-  ( A C_ ( C u. B ) <-> ( A \ C ) C_ B )
11 9 10 bitri 
 |-  ( A C_ ( B u. C ) <-> ( A \ C ) C_ B )
12 difexg 
 |-  ( A e. _V -> ( A \ C ) e. _V )
13 elpwg 
 |-  ( ( A \ C ) e. _V -> ( ( A \ C ) e. ~P B <-> ( A \ C ) C_ B ) )
14 12 13 syl 
 |-  ( A e. _V -> ( ( A \ C ) e. ~P B <-> ( A \ C ) C_ B ) )
15 11 14 bitr4id 
 |-  ( A e. _V -> ( A C_ ( B u. C ) <-> ( A \ C ) e. ~P B ) )
16 7 15 bitrd 
 |-  ( A e. _V -> ( A e. ~P ( B u. C ) <-> ( A \ C ) e. ~P B ) )
17 2 6 16 pm5.21nii 
 |-  ( A e. ~P ( B u. C ) <-> ( A \ C ) e. ~P B )