Metamath Proof Explorer

Theorem sprvalpwn0

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

Ref Expression
Assertion sprvalpwn0 
|- ( V e. W -> ( Pairs ` V ) = { p e. ( ~P V \ { (/) } ) | E. a e. V E. b e. V p = { a , b } } )

Proof

Step Hyp Ref Expression
1 sprvalpw 
 |-  ( V e. W -> ( Pairs ` V ) = { p e. ~P V | E. a e. V E. b e. V p = { a , b } } )
2 id 
 |-  ( p = { a , b } -> p = { a , b } )
3 vex 
 |-  a e. _V
4 3 prnz 
 |-  { a , b } =/= (/)
5 4 a1i 
 |-  ( p = { a , b } -> { a , b } =/= (/) )
6 2 5 eqnetrd 
 |-  ( p = { a , b } -> p =/= (/) )
7 6 a1i 
 |-  ( ( a e. V /\ b e. V ) -> ( p = { a , b } -> p =/= (/) ) )
8 7 rexlimivv 
 |-  ( E. a e. V E. b e. V p = { a , b } -> p =/= (/) )
9 8 adantl 
 |-  ( ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) -> p =/= (/) )
10 9 pm4.71ri 
 |-  ( ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) <-> ( p =/= (/) /\ ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) ) )
11 ancom 
 |-  ( ( p =/= (/) /\ p e. ~P V ) <-> ( p e. ~P V /\ p =/= (/) ) )
12 11 anbi1i 
 |-  ( ( ( p =/= (/) /\ p e. ~P V ) /\ E. a e. V E. b e. V p = { a , b } ) <-> ( ( p e. ~P V /\ p =/= (/) ) /\ E. a e. V E. b e. V p = { a , b } ) )
13 anass 
 |-  ( ( ( p =/= (/) /\ p e. ~P V ) /\ E. a e. V E. b e. V p = { a , b } ) <-> ( p =/= (/) /\ ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) ) )
14 eldifsn 
 |-  ( p e. ( ~P V \ { (/) } ) <-> ( p e. ~P V /\ p =/= (/) ) )
15 14 bicomi 
 |-  ( ( p e. ~P V /\ p =/= (/) ) <-> p e. ( ~P V \ { (/) } ) )
16 15 anbi1i 
 |-  ( ( ( p e. ~P V /\ p =/= (/) ) /\ E. a e. V E. b e. V p = { a , b } ) <-> ( p e. ( ~P V \ { (/) } ) /\ E. a e. V E. b e. V p = { a , b } ) )
17 12 13 16 3bitr3i 
 |-  ( ( p =/= (/) /\ ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) ) <-> ( p e. ( ~P V \ { (/) } ) /\ E. a e. V E. b e. V p = { a , b } ) )
18 10 17 bitri 
 |-  ( ( p e. ~P V /\ E. a e. V E. b e. V p = { a , b } ) <-> ( p e. ( ~P V \ { (/) } ) /\ E. a e. V E. b e. V p = { a , b } ) )
19 18 rabbia2 
 |-  { p e. ~P V | E. a e. V E. b e. V p = { a , b } } = { p e. ( ~P V \ { (/) } ) | E. a e. V E. b e. V p = { a , b } }
20 1 19 eqtrdi 
 |-  ( V e. W -> ( Pairs ` V ) = { p e. ( ~P V \ { (/) } ) | E. a e. V E. b e. V p = { a , b } } )