Theorem prssspr

Description: An element of a subset 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	prssspr	|- ( ( P C_ ( Pairs ` V ) /\ X e. P ) -> E. a e. V E. b e. V X = { a , b } )

Proof

Step	Hyp	Ref	Expression
1		ssel2	|- ( ( P C_ ( Pairs ` V ) /\ X e. P ) -> X e. ( Pairs ` V ) )
2		sprel	|- ( X e. ( Pairs ` V ) -> E. a e. V E. b e. V X = { a , b } )
3	1 2	syl	|- ( ( P C_ ( Pairs ` V ) /\ X e. P ) -> E. a e. V E. b e. V X = { a , b } )