Metamath Proof Explorer


Theorem prprvalpw

Description: The set of all proper unordered pairs over a given set V , expressed by a restricted class abstraction. (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprvalpw ( 𝑉𝑊 → ( Pairsproper𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )

Proof

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