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 } )