Metamath Proof Explorer


Theorem sprvalpwle2

Description: The set of all unordered pairs over a given set V , expressed by a restricted class abstraction. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion sprvalpwle2
|- ( V e. W -> ( Pairs ` V ) = { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )

Proof

Step Hyp Ref Expression
1 sprvalpwn0
 |-  ( V e. W -> ( Pairs ` V ) = { p e. ( ~P V \ { (/) } ) | E. a e. V E. b e. V p = { a , b } } )
2 hashle2prv
 |-  ( p e. ( ~P V \ { (/) } ) -> ( ( # ` p ) <_ 2 <-> E. a e. V E. b e. V p = { a , b } ) )
3 2 adantl
 |-  ( ( V e. W /\ p e. ( ~P V \ { (/) } ) ) -> ( ( # ` p ) <_ 2 <-> E. a e. V E. b e. V p = { a , b } ) )
4 3 bicomd
 |-  ( ( V e. W /\ p e. ( ~P V \ { (/) } ) ) -> ( E. a e. V E. b e. V p = { a , b } <-> ( # ` p ) <_ 2 ) )
5 4 rabbidva
 |-  ( V e. W -> { p e. ( ~P V \ { (/) } ) | E. a e. V E. b e. V p = { a , b } } = { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
6 1 5 eqtrd
 |-  ( V e. W -> ( Pairs ` V ) = { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )