Theorem sprssspr

Description: The set of all unordered pairs over a given set V is a subset of the set of all unordered pairs. (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	sprssspr	|- ( Pairs ` V ) C_ { p | E. a E. b p = { a , b } }

Proof

Step	Hyp	Ref	Expression
1		sprval	|- ( V e. _V -> ( Pairs ` V ) = { p | E. a e. V E. b e. V p = { a , b } } )
2		r2ex	|- ( E. a e. V E. b e. V p = { a , b } <-> E. a E. b ( ( a e. V /\ b e. V ) /\ p = { a , b } ) )
3		simpr	|- ( ( ( a e. V /\ b e. V ) /\ p = { a , b } ) -> p = { a , b } )
4	3	2eximi	|- ( E. a E. b ( ( a e. V /\ b e. V ) /\ p = { a , b } ) -> E. a E. b p = { a , b } )
5	2 4	sylbi	|- ( E. a e. V E. b e. V p = { a , b } -> E. a E. b p = { a , b } )
6	5	ax-gen	|- A. p ( E. a e. V E. b e. V p = { a , b } -> E. a E. b p = { a , b } )
7	6	a1i	|- ( V e. _V -> A. p ( E. a e. V E. b e. V p = { a , b } -> E. a E. b p = { a , b } ) )
8		ss2ab	|- ( { p | E. a e. V E. b e. V p = { a , b } } C_ { p | E. a E. b p = { a , b } } <-> A. p ( E. a e. V E. b e. V p = { a , b } -> E. a E. b p = { a , b } ) )
9	7 8	sylibr	|- ( V e. _V -> { p | E. a e. V E. b e. V p = { a , b } } C_ { p | E. a E. b p = { a , b } } )
10	1 9	eqsstrd	|- ( V e. _V -> ( Pairs ` V ) C_ { p | E. a E. b p = { a , b } } )
11		fvprc	|- ( -. V e. _V -> ( Pairs ` V ) = (/) )
12		0ss	|- (/) C_ { p | E. a E. b p = { a , b } }
13	12	a1i	|- ( -. V e. _V -> (/) C_ { p | E. a E. b p = { a , b } } )
14	11 13	eqsstrd	|- ( -. V e. _V -> ( Pairs ` V ) C_ { p | E. a E. b p = { a , b } } )
15	10 14	pm2.61i	|- ( Pairs ` V ) C_ { p | E. a E. b p = { a , b } }