Theorem prprspr2

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

	Ref	Expression
Assertion	prprspr2	|- ( PrPairs ` V ) = { p e. ( Pairs ` V ) | ( # ` p ) = 2 }

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	1	abeq2d	|- ( V e. _V -> ( p e. ( Pairs ` V ) <-> E. a e. V E. b e. V p = { a , b } ) )
3	2	anbi1d	|- ( V e. _V -> ( ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) <-> ( E. a e. V E. b e. V p = { a , b } /\ ( # ` p ) = 2 ) ) )
4		r19.41vv	|- ( E. a e. V E. b e. V ( p = { a , b } /\ ( # ` p ) = 2 ) <-> ( E. a e. V E. b e. V p = { a , b } /\ ( # ` p ) = 2 ) )
5		fveqeq2	|- ( p = { a , b } -> ( ( # ` p ) = 2 <-> ( # ` { a , b } ) = 2 ) )
6		hashprg	|- ( ( a e. _V /\ b e. _V ) -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
7	6	el2v	|- ( a =/= b <-> ( # ` { a , b } ) = 2 )
8	5 7	bitr4di	|- ( p = { a , b } -> ( ( # ` p ) = 2 <-> a =/= b ) )
9	8	pm5.32i	|- ( ( p = { a , b } /\ ( # ` p ) = 2 ) <-> ( p = { a , b } /\ a =/= b ) )
10	9	biancomi	|- ( ( p = { a , b } /\ ( # ` p ) = 2 ) <-> ( a =/= b /\ p = { a , b } ) )
11	10	a1i	|- ( ( V e. _V /\ ( a e. V /\ b e. V ) ) -> ( ( p = { a , b } /\ ( # ` p ) = 2 ) <-> ( a =/= b /\ p = { a , b } ) ) )
12	11	2rexbidva	|- ( V e. _V -> ( E. a e. V E. b e. V ( p = { a , b } /\ ( # ` p ) = 2 ) <-> E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) ) )
13	4 12	bitr3id	|- ( V e. _V -> ( ( E. a e. V E. b e. V p = { a , b } /\ ( # ` p ) = 2 ) <-> E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) ) )
14	3 13	bitrd	|- ( V e. _V -> ( ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) <-> E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) ) )
15	14	abbidv	|- ( V e. _V -> { p | ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) } = { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )
16		df-rab	|- { p e. ( Pairs ` V ) | ( # ` p ) = 2 } = { p | ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) }
17	16	a1i	|- ( V e. _V -> { p e. ( Pairs ` V ) | ( # ` p ) = 2 } = { p | ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) } )
18		prprval	|- ( V e. _V -> ( PrPairs ` V ) = { p | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )
19	15 17 18	3eqtr4rd	|- ( V e. _V -> ( PrPairs ` V ) = { p e. ( Pairs ` V ) | ( # ` p ) = 2 } )
20		rab0	|- { p e. (/) | ( # ` p ) = 2 } = (/)
21	20	a1i	|- ( -. V e. _V -> { p e. (/) | ( # ` p ) = 2 } = (/) )
22		fvprc	|- ( -. V e. _V -> ( Pairs ` V ) = (/) )
23	22	rabeqdv	|- ( -. V e. _V -> { p e. ( Pairs ` V ) | ( # ` p ) = 2 } = { p e. (/) | ( # ` p ) = 2 } )
24		fvprc	|- ( -. V e. _V -> ( PrPairs ` V ) = (/) )
25	21 23 24	3eqtr4rd	|- ( -. V e. _V -> ( PrPairs ` V ) = { p e. ( Pairs ` V ) | ( # ` p ) = 2 } )
26	19 25	pm2.61i	|- ( PrPairs ` V ) = { p e. ( Pairs ` V ) | ( # ` p ) = 2 }