Metamath Proof Explorer


Theorem prprsprreu

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

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

Proof

Step Hyp Ref Expression
1 prprspr2
 |-  ( PrPairs ` V ) = { p e. ( Pairs ` V ) | ( # ` p ) = 2 }
2 1 rabeq2i
 |-  ( p e. ( PrPairs ` V ) <-> ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) )
3 2 a1i
 |-  ( V e. W -> ( p e. ( PrPairs ` V ) <-> ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) ) )
4 3 anbi1d
 |-  ( V e. W -> ( ( p e. ( PrPairs ` V ) /\ ph ) <-> ( ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) /\ ph ) ) )
5 anass
 |-  ( ( ( p e. ( Pairs ` V ) /\ ( # ` p ) = 2 ) /\ ph ) <-> ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) )
6 4 5 bitrdi
 |-  ( V e. W -> ( ( p e. ( PrPairs ` V ) /\ ph ) <-> ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) ) )
7 6 eubidv
 |-  ( V e. W -> ( E! p ( p e. ( PrPairs ` V ) /\ ph ) <-> E! p ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) ) )
8 df-reu
 |-  ( E! p e. ( PrPairs ` V ) ph <-> E! p ( p e. ( PrPairs ` V ) /\ ph ) )
9 df-reu
 |-  ( E! p e. ( Pairs ` V ) ( ( # ` p ) = 2 /\ ph ) <-> E! p ( p e. ( Pairs ` V ) /\ ( ( # ` p ) = 2 /\ ph ) ) )
10 7 8 9 3bitr4g
 |-  ( V e. W -> ( E! p e. ( PrPairs ` V ) ph <-> E! p e. ( Pairs ` V ) ( ( # ` p ) = 2 /\ ph ) ) )