Theorem sprvalpw

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

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

Proof

Step	Hyp	Ref	Expression
1		sprval	|- ( V e. W -> ( Pairs ` V ) = { p | E. a e. V E. b e. V p = { a , b } } )
2		prssi	|- ( ( a e. V /\ b e. V ) -> { a , b } C_ V )
3		eleq1	|- ( p = { a , b } -> ( p e. ~P V <-> { a , b } e. ~P V ) )
4		prex	|- { a , b } e. _V
5	4	elpw	|- ( { a , b } e. ~P V <-> { a , b } C_ V )
6	3 5	bitrdi	|- ( p = { a , b } -> ( p e. ~P V <-> { a , b } C_ V ) )
7	2 6	syl5ibrcom	|- ( ( a e. V /\ b e. V ) -> ( p = { a , b } -> p e. ~P V ) )
8	7	rexlimivv	|- ( E. a e. V E. b e. V p = { a , b } -> p e. ~P V )
9	8	pm4.71ri	|- ( E. a e. V E. b e. V p = { a , b } <-> ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) )
10	9	a1i	|- ( V e. W -> ( E. a e. V E. b e. V p = { a , b } <-> ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) ) )
11	10	abbidv	|- ( V e. W -> { p | E. a e. V E. b e. V p = { a , b } } = { p | ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) } )
12		df-rab	|- { p e. ~P V | E. a e. V E. b e. V p = { a , b } } = { p | ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) }
13	11 12	eqtr4di	|- ( V e. W -> { p | E. a e. V E. b e. V p = { a , b } } = { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )
14	1 13	eqtrd	|- ( V e. W -> ( Pairs ` V ) = { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )