Theorem sprval

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

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

Proof

Step	Hyp	Ref	Expression
1		df-spr	|- Pairs = ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } )
2	1	a1i	|- ( V e. W -> Pairs = ( v e. _V |-> { p | E. a e. v E. b e. v p = { a , b } } ) )
3		id	|- ( v = V -> v = V )
4		rexeq	|- ( v = V -> ( E. b e. v p = { a , b } <-> E. b e. V p = { a , b } ) )
5	3 4	rexeqbidv	|- ( v = V -> ( E. a e. v E. b e. v p = { a , b } <-> E. a e. V E. b e. V p = { a , b } ) )
6	5	adantl	|- ( ( V e. W /\ v = V ) -> ( E. a e. v E. b e. v p = { a , b } <-> E. a e. V E. b e. V p = { a , b } ) )
7	6	abbidv	|- ( ( V e. W /\ v = V ) -> { p | E. a e. v E. b e. v p = { a , b } } = { p | E. a e. V E. b e. V p = { a , b } } )
8		elex	|- ( V e. W -> V e. _V )
9		zfpair2	|- { a , b } e. _V
10		eueq	|- ( { a , b } e. _V <-> E! p p = { a , b } )
11	9 10	mpbi	|- E! p p = { a , b }
12		euabex	|- ( E! p p = { a , b } -> { p | p = { a , b } } e. _V )
13	11 12	mp1i	|- ( V e. W -> { p | p = { a , b } } e. _V )
14	13	ralrimivw	|- ( V e. W -> A. b e. V { p | p = { a , b } } e. _V )
15		abrexex2g	|- ( ( V e. W /\ A. b e. V { p | p = { a , b } } e. _V ) -> { p | E. b e. V p = { a , b } } e. _V )
16	14 15	mpdan	|- ( V e. W -> { p | E. b e. V p = { a , b } } e. _V )
17	16	ralrimivw	|- ( V e. W -> A. a e. V { p | E. b e. V p = { a , b } } e. _V )
18		abrexex2g	|- ( ( V e. W /\ A. a e. V { p | E. b e. V p = { a , b } } e. _V ) -> { p | E. a e. V E. b e. V p = { a , b } } e. _V )
19	17 18	mpdan	|- ( V e. W -> { p | E. a e. V E. b e. V p = { a , b } } e. _V )
20	2 7 8 19	fvmptd	|- ( V e. W -> ( Pairs ` V ) = { p | E. a e. V E. b e. V p = { a , b } } )