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	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )

Proof

Step	Hyp	Ref	Expression
1		sprvalpwn0	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
2		hashle2prv	⊢ ( 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ( ♯ ‘ 𝑝 ) ≤ 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
3	2	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ) → ( ( ♯ ‘ 𝑝 ) ≤ 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
4	3	bicomd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ↔ ( ♯ ‘ 𝑝 ) ≤ 2 ) )
5	4	rabbidva	⊢ ( 𝑉 ∈ 𝑊 → { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
6	1 5	eqtrd	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )