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 }