Metamath Proof Explorer


Theorem prprrab

Description: The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020)

Ref Expression
Assertion prprrab
|- { x e. ( ~P A \ { (/) } ) | ( # ` x ) = 2 } = { x e. ~P A | ( # ` x ) = 2 }

Proof

Step Hyp Ref Expression
1 2ne0
 |-  2 =/= 0
2 1 neii
 |-  -. 2 = 0
3 eqeq1
 |-  ( ( # ` x ) = 2 -> ( ( # ` x ) = 0 <-> 2 = 0 ) )
4 2 3 mtbiri
 |-  ( ( # ` x ) = 2 -> -. ( # ` x ) = 0 )
5 hasheq0
 |-  ( x e. _V -> ( ( # ` x ) = 0 <-> x = (/) ) )
6 5 bicomd
 |-  ( x e. _V -> ( x = (/) <-> ( # ` x ) = 0 ) )
7 6 necon3abid
 |-  ( x e. _V -> ( x =/= (/) <-> -. ( # ` x ) = 0 ) )
8 7 elv
 |-  ( x =/= (/) <-> -. ( # ` x ) = 0 )
9 4 8 sylibr
 |-  ( ( # ` x ) = 2 -> x =/= (/) )
10 9 biantrud
 |-  ( ( # ` x ) = 2 -> ( x e. ~P A <-> ( x e. ~P A /\ x =/= (/) ) ) )
11 eldifsn
 |-  ( x e. ( ~P A \ { (/) } ) <-> ( x e. ~P A /\ x =/= (/) ) )
12 10 11 bitr4di
 |-  ( ( # ` x ) = 2 -> ( x e. ~P A <-> x e. ( ~P A \ { (/) } ) ) )
13 12 pm5.32ri
 |-  ( ( x e. ~P A /\ ( # ` x ) = 2 ) <-> ( x e. ( ~P A \ { (/) } ) /\ ( # ` x ) = 2 ) )
14 13 abbii
 |-  { x | ( x e. ~P A /\ ( # ` x ) = 2 ) } = { x | ( x e. ( ~P A \ { (/) } ) /\ ( # ` x ) = 2 ) }
15 df-rab
 |-  { x e. ~P A | ( # ` x ) = 2 } = { x | ( x e. ~P A /\ ( # ` x ) = 2 ) }
16 df-rab
 |-  { x e. ( ~P A \ { (/) } ) | ( # ` x ) = 2 } = { x | ( x e. ( ~P A \ { (/) } ) /\ ( # ` x ) = 2 ) }
17 14 15 16 3eqtr4ri
 |-  { x e. ( ~P A \ { (/) } ) | ( # ` x ) = 2 } = { x e. ~P A | ( # ` x ) = 2 }