Metamath Proof Explorer


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 Pairs V | p = 2

Proof

Step Hyp Ref Expression
1 sprval V V Pairs V = p | a V b V p = a b
2 1 abeq2d V V p Pairs V a V b V p = a b
3 2 anbi1d V V p Pairs V p = 2 a V b V p = a b p = 2
4 r19.41vv a V b V p = a b p = 2 a V b V p = a b p = 2
5 fveqeq2 p = a b p = 2 a b = 2
6 hashprg a V b 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 V a V b V p = a b p = 2 a b p = a b
12 11 2rexbidva V V a V b V p = a b p = 2 a V b V a b p = a b
13 4 12 bitr3id V V a V b V p = a b p = 2 a V b V a b p = a b
14 3 13 bitrd V V p Pairs V p = 2 a V b V a b p = a b
15 14 abbidv V V p | p Pairs V p = 2 = p | a V b V a b p = a b
16 df-rab p Pairs V | p = 2 = p | p Pairs V p = 2
17 16 a1i V V p Pairs V | p = 2 = p | p Pairs V p = 2
18 prprval V V PrPairs V = p | a V b V a b p = a b
19 15 17 18 3eqtr4rd V V PrPairs V = p Pairs V | p = 2
20 rab0 p | p = 2 =
21 20 a1i ¬ V V p | p = 2 =
22 fvprc ¬ V V Pairs V =
23 22 rabeqdv ¬ V V p Pairs V | p = 2 = p | p = 2
24 fvprc ¬ V V PrPairs V =
25 21 23 24 3eqtr4rd ¬ V V PrPairs V = p Pairs V | p = 2
26 19 25 pm2.61i PrPairs V = p Pairs V | p = 2