Theorem prprvalpw

Description: The set of all proper unordered pairs over a given set V , expressed by a restricted class abstraction. (Contributed by AV, 29-Apr-2023)

	Ref	Expression
Assertion	prprvalpw	|- ( V e. W -> ( PrPairs ` V ) = { p e. ~P V | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )

Proof

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