Metamath Proof Explorer

Theorem prprreueq

Description: There is a unique proper unordered pair over a given set V fulfilling a wff iff there is a unique subset of V of size two fulfilling this wff. (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprreueq 
|- ( V e. W -> ( E! p e. ( PrPairs ` V ) ph <-> E! p e. ~P V ( ( # ` p ) = 2 /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 prprelb 
 |-  ( V e. W -> ( p e. ( PrPairs ` V ) <-> ( p e. ~P V /\ ( # ` p ) = 2 ) ) )
2 1 anbi1d 
 |-  ( V e. W -> ( ( p e. ( PrPairs ` V ) /\ ph ) <-> ( ( p e. ~P V /\ ( # ` p ) = 2 ) /\ ph ) ) )
3 anass 
 |-  ( ( ( p e. ~P V /\ ( # ` p ) = 2 ) /\ ph ) <-> ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) )
4 2 3 bitrdi 
 |-  ( V e. W -> ( ( p e. ( PrPairs ` V ) /\ ph ) <-> ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) ) )
5 4 eubidv 
 |-  ( V e. W -> ( E! p ( p e. ( PrPairs ` V ) /\ ph ) <-> E! p ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) ) )
6 df-reu 
 |-  ( E! p e. ( PrPairs ` V ) ph <-> E! p ( p e. ( PrPairs ` V ) /\ ph ) )
7 df-reu 
 |-  ( E! p e. ~P V ( ( # ` p ) = 2 /\ ph ) <-> E! p ( p e. ~P V /\ ( ( # ` p ) = 2 /\ ph ) ) )
8 5 6 7 3bitr4g 
 |-  ( V e. W -> ( E! p e. ( PrPairs ` V ) ph <-> E! p e. ~P V ( ( # ` p ) = 2 /\ ph ) ) )