This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }