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

Proof

Step	Hyp	Ref	Expression
1		sprvalpw	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
2		id	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → 𝑝 = { 𝑎 , 𝑏 } )
3		vex	⊢ 𝑎 ∈ V
4	3	prnz	⊢ { 𝑎 , 𝑏 } ≠ ∅
5	4	a1i	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → { 𝑎 , 𝑏 } ≠ ∅ )
6	2 5	eqnetrd	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → 𝑝 ≠ ∅ )
7	6	a1i	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑝 = { 𝑎 , 𝑏 } → 𝑝 ≠ ∅ ) )
8	7	rexlimivv	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } → 𝑝 ≠ ∅ )
9	8	adantl	⊢ ( ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) → 𝑝 ≠ ∅ )
10	9	pm4.71ri	⊢ ( ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑝 ≠ ∅ ∧ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ) )
11		ancom	⊢ ( ( 𝑝 ≠ ∅ ∧ 𝑝 ∈ 𝒫 𝑉 ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅ ) )
12	11	anbi1i	⊢ ( ( ( 𝑝 ≠ ∅ ∧ 𝑝 ∈ 𝒫 𝑉 ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( ( 𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅ ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
13		anass	⊢ ( ( ( 𝑝 ≠ ∅ ∧ 𝑝 ∈ 𝒫 𝑉 ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑝 ≠ ∅ ∧ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ) )
14		eldifsn	⊢ ( 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅ ) )
15	14	bicomi	⊢ ( ( 𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅ ) ↔ 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
16	15	anbi1i	⊢ ( ( ( 𝑝 ∈ 𝒫 𝑉 ∧ 𝑝 ≠ ∅ ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
17	12 13 16	3bitr3i	⊢ ( ( 𝑝 ≠ ∅ ∧ ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ) ↔ ( 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
18	10 17	bitri	⊢ ( ( 𝑝 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
19	18	rabbia2	⊢ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } }
20	1 19	eqtrdi	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )