Theorem sprel

Description: An element of the set of all unordered pairs over a given set V is a pair of elements of the set V . (Contributed by AV, 22-Nov-2021)

	Ref	Expression
Assertion	sprel	|- ( X e. ( Pairs ` V ) -> E. a e. V E. b e. V X = { a , b } )

Proof

Step	Hyp	Ref	Expression
1		elfvex	|- ( X e. ( Pairs ` V ) -> V e. _V )
2		sprvalpw	|- ( V e. _V -> ( Pairs ` V ) = { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )
3	2	eleq2d	|- ( V e. _V -> ( X e. ( Pairs ` V ) <-> X e. { p e. ~P V | E. a e. V E. b e. V p = { a , b } } ) )
4		eqeq1	|- ( p = X -> ( p = { a , b } <-> X = { a , b } ) )
5	4	2rexbidv	|- ( p = X -> ( E. a e. V E. b e. V p = { a , b } <-> E. a e. V E. b e. V X = { a , b } ) )
6	5	elrab	|- ( X e. { p e. ~P V | E. a e. V E. b e. V p = { a , b } } <-> ( X e. ~P V /\ E. a e. V E. b e. V X = { a , b } ) )
7	6	simprbi	|- ( X e. { p e. ~P V | E. a e. V E. b e. V p = { a , b } } -> E. a e. V E. b e. V X = { a , b } )
8	3 7	syl6bi	|- ( V e. _V -> ( X e. ( Pairs ` V ) -> E. a e. V E. b e. V X = { a , b } ) )
9	1 8	mpcom	|- ( X e. ( Pairs ` V ) -> E. a e. V E. b e. V X = { a , b } )