Theorem prprval

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

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

Proof

Step	Hyp	Ref	Expression
1		df-prpr	|- PrPairs = ( v e. _V |-> { p | E. a e. v E. b e. v ( a =/= b /\ p = { a , b } ) } )
2		rexeq	|- ( v = V -> ( E. b e. v ( a =/= b /\ p = { a , b } ) <-> E. b e. V ( a =/= b /\ p = { a , b } ) ) )
3	2	rexeqbi1dv	|- ( v = V -> ( E. a e. v E. b e. v ( a =/= b /\ p = { a , b } ) <-> E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) ) )
4	3	abbidv	|- ( v = V -> { p | E. a e. v E. b e. v ( a =/= b /\ p = { a , b } ) } = { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )
5	4	adantl	|- ( ( V e. W /\ v = V ) -> { p | E. a e. v E. b e. v ( a =/= b /\ p = { a , b } ) } = { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )
6		elex	|- ( V e. W -> V e. _V )
7		simpr	|- ( ( a =/= b /\ p = { a , b } ) -> p = { a , b } )
8	7	ss2abi	|- { p | ( a =/= b /\ p = { a , b } ) } C_ { p | p = { a , b } }
9		zfpair2	|- { a , b } e. _V
10	9	eueqi	|- E! p p = { a , b }
11		euabex	|- ( E! p p = { a , b } -> { p | p = { a , b } } e. _V )
12	10 11	mp1i	|- ( V e. W -> { p | p = { a , b } } e. _V )
13		ssexg	|- ( ( { p | ( a =/= b /\ p = { a , b } ) } C_ { p | p = { a , b } } /\ { p | p = { a , b } } e. _V ) -> { p | ( a =/= b /\ p = { a , b } ) } e. _V )
14	8 12 13	sylancr	|- ( V e. W -> { p | ( a =/= b /\ p = { a , b } ) } e. _V )
15	14	ralrimivw	|- ( V e. W -> A. b e. V { p | ( a =/= b /\ p = { a , b } ) } e. _V )
16		abrexex2g	|- ( ( V e. W /\ A. b e. V { p | ( a =/= b /\ p = { a , b } ) } e. _V ) -> { p | E. b e. V ( a =/= b /\ p = { a , b } ) } e. _V )
17	15 16	mpdan	|- ( V e. W -> { p | E. b e. V ( a =/= b /\ p = { a , b } ) } e. _V )
18	17	ralrimivw	|- ( V e. W -> A. a e. V { p | E. b e. V ( a =/= b /\ p = { a , b } ) } e. _V )
19		abrexex2g	|- ( ( V e. W /\ A. a e. V { p | E. b e. V ( a =/= b /\ p = { a , b } ) } e. _V ) -> { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } e. _V )
20	18 19	mpdan	|- ( V e. W -> { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } e. _V )
21	1 5 6 20	fvmptd2	|- ( V e. W -> ( PrPairs ` V ) = { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )