Metamath Proof Explorer


Theorem sprvalpw

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 sprvalpw ( 𝑉𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } )

Proof

Step Hyp Ref Expression
1 sprval ( 𝑉𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } )
2 prssi ( ( 𝑎𝑉𝑏𝑉 ) → { 𝑎 , 𝑏 } ⊆ 𝑉 )
3 eleq1 ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) )
4 prex { 𝑎 , 𝑏 } ∈ V
5 4 elpw ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ⊆ 𝑉 )
6 3 5 bitrdi ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ⊆ 𝑉 ) )
7 2 6 syl5ibrcom ( ( 𝑎𝑉𝑏𝑉 ) → ( 𝑝 = { 𝑎 , 𝑏 } → 𝑝 ∈ 𝒫 𝑉 ) )
8 7 rexlimivv ( ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } → 𝑝 ∈ 𝒫 𝑉 )
9 8 pm4.71ri ( ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
10 9 a1i ( 𝑉𝑊 → ( ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } ) ) )
11 10 abbidv ( 𝑉𝑊 → { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∣ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } ) } )
12 df-rab { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∣ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } ) }
13 11 12 eqtr4di ( 𝑉𝑊 → { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } )
14 1 13 eqtrd ( 𝑉𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎𝑉𝑏𝑉 𝑝 = { 𝑎 , 𝑏 } } )