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

Metamath Proof Explorer

Theorem pwpr

Description: The power set of an unordered pair. (Contributed by NM, 1-May-2009)

Ref Expression
Assertion pwpr 
|- ~P { A , B } = ( { (/) , { A } } u. { { B } , { A , B } } )

Proof

Step Hyp Ref Expression
1 sspr 
 |-  ( x C_ { A , B } <-> ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) )
2 vex 
 |-  x e. _V
3 2 elpr 
 |-  ( x e. { (/) , { A } } <-> ( x = (/) \/ x = { A } ) )
4 2 elpr 
 |-  ( x e. { { B } , { A , B } } <-> ( x = { B } \/ x = { A , B } ) )
5 3 4 orbi12i 
 |-  ( ( x e. { (/) , { A } } \/ x e. { { B } , { A , B } } ) <-> ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) )
6 1 5 bitr4i 
 |-  ( x C_ { A , B } <-> ( x e. { (/) , { A } } \/ x e. { { B } , { A , B } } ) )
7 velpw 
 |-  ( x e. ~P { A , B } <-> x C_ { A , B } )
8 elun 
 |-  ( x e. ( { (/) , { A } } u. { { B } , { A , B } } ) <-> ( x e. { (/) , { A } } \/ x e. { { B } , { A , B } } ) )
9 6 7 8 3bitr4i 
 |-  ( x e. ~P { A , B } <-> x e. ( { (/) , { A } } u. { { B } , { A , B } } ) )
10 9 eqriv 
 |-  ~P { A , B } = ( { (/) , { A } } u. { { B } , { A , B } } )