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 } )