Metamath Proof Explorer


Theorem prprelprb

Description: A set is an element of the set of all proper unordered pairs over a given set X iff it is a pair of different elements of the set X . (Contributed by AV, 7-May-2023)

Ref Expression
Assertion prprelprb P PrPairs X X V a X b X P = a b a b

Proof

Step Hyp Ref Expression
1 prprvalpw X V PrPairs X = p 𝒫 X | a X b X a b p = a b
2 1 eleq2d X V P PrPairs X P p 𝒫 X | a X b X a b p = a b
3 eqeq1 p = P p = a b P = a b
4 3 anbi2d p = P a b p = a b a b P = a b
5 4 2rexbidv p = P a X b X a b p = a b a X b X a b P = a b
6 5 elrab P p 𝒫 X | a X b X a b p = a b P 𝒫 X a X b X a b P = a b
7 2 6 bitrdi X V P PrPairs X P 𝒫 X a X b X a b P = a b
8 pm3.22 a b P = a b P = a b a b
9 8 a1i P 𝒫 X a X b X a b P = a b P = a b a b
10 9 reximdvva P 𝒫 X a X b X a b P = a b a X b X P = a b a b
11 10 imp P 𝒫 X a X b X a b P = a b a X b X P = a b a b
12 11 anim2i X V P 𝒫 X a X b X a b P = a b X V a X b X P = a b a b
13 12 ex X V P 𝒫 X a X b X a b P = a b X V a X b X P = a b a b
14 simpr X V a X b X P = a b a b P = a b a b
15 14 ancomd X V a X b X P = a b a b a b P = a b
16 prelpwi a X b X a b 𝒫 X
17 16 adantl X V a X b X a b 𝒫 X
18 17 adantr X V a X b X P = a b a b a b 𝒫 X
19 eleq1 P = a b P 𝒫 X a b 𝒫 X
20 19 adantr P = a b a b P 𝒫 X a b 𝒫 X
21 20 adantl X V a X b X P = a b a b P 𝒫 X a b 𝒫 X
22 18 21 mpbird X V a X b X P = a b a b P 𝒫 X
23 15 22 jca X V a X b X P = a b a b a b P = a b P 𝒫 X
24 23 ex X V a X b X P = a b a b a b P = a b P 𝒫 X
25 24 reximdvva X V a X b X P = a b a b a X b X a b P = a b P 𝒫 X
26 25 imp X V a X b X P = a b a b a X b X a b P = a b P 𝒫 X
27 r19.41vv a X b X a b P = a b P 𝒫 X a X b X a b P = a b P 𝒫 X
28 27 biancomi a X b X a b P = a b P 𝒫 X P 𝒫 X a X b X a b P = a b
29 26 28 sylib X V a X b X P = a b a b P 𝒫 X a X b X a b P = a b
30 13 29 impbid1 X V P 𝒫 X a X b X a b P = a b X V a X b X P = a b a b
31 7 30 bitrd X V P PrPairs X X V a X b X P = a b a b
32 fvprc ¬ X V PrPairs X =
33 32 eleq2d ¬ X V P PrPairs X P
34 noel ¬ P
35 pm2.21 ¬ P P X V a X b X P = a b a b
36 34 35 mp1i ¬ X V P X V a X b X P = a b a b
37 pm2.21 ¬ X V X V a X b X P = a b a b P
38 37 impd ¬ X V X V a X b X P = a b a b P
39 36 38 impbid ¬ X V P X V a X b X P = a b a b
40 33 39 bitrd ¬ X V P PrPairs X X V a X b X P = a b a b
41 31 40 pm2.61i P PrPairs X X V a X b X P = a b a b