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

Metamath Proof Explorer

Theorem hash2sspr

Description: A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017) (Proof shortened by AV, 4-Nov-2020)

Ref Expression
Assertion hash2sspr 
|- ( ( P e. ~P V /\ ( # ` P ) = 2 ) -> E. a e. V E. b e. V P = { a , b } )

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( p = P -> ( ( # ` p ) = 2 <-> ( # ` P ) = 2 ) )
2 1 elrab 
 |-  ( P e. { p e. ~P V | ( # ` p ) = 2 } <-> ( P e. ~P V /\ ( # ` P ) = 2 ) )
3 elss2prb 
 |-  ( P e. { p e. ~P V | ( # ` p ) = 2 } <-> E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) )
4 simpr 
 |-  ( ( a =/= b /\ P = { a , b } ) -> P = { a , b } )
5 4 reximi 
 |-  ( E. b e. V ( a =/= b /\ P = { a , b } ) -> E. b e. V P = { a , b } )
6 5 reximi 
 |-  ( E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) -> E. a e. V E. b e. V P = { a , b } )
7 3 6 sylbi 
 |-  ( P e. { p e. ~P V | ( # ` p ) = 2 } -> E. a e. V E. b e. V P = { a , b } )
8 2 7 sylbir 
 |-  ( ( P e. ~P V /\ ( # ` P ) = 2 ) -> E. a e. V E. b e. V P = { a , b } )