Theorem sprel

Description: An element of the set of all unordered pairs over a given set V is a pair of elements of the set V . (Contributed by AV, 22-Nov-2021)

	Ref	Expression
Assertion	sprel	⊢ ( 𝑋 ∈ ( Pairs ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝑋 ∈ ( Pairs ‘ 𝑉 ) → 𝑉 ∈ V )
2		sprvalpw	⊢ ( 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
3	2	eleq2d	⊢ ( 𝑉 ∈ V → ( 𝑋 ∈ ( Pairs ‘ 𝑉 ) ↔ 𝑋 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ) )
4		eqeq1	⊢ ( 𝑝 = 𝑋 → ( 𝑝 = { 𝑎 , 𝑏 } ↔ 𝑋 = { 𝑎 , 𝑏 } ) )
5	4	2rexbidv	⊢ ( 𝑝 = 𝑋 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } ) )
6	5	elrab	⊢ ( 𝑋 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ↔ ( 𝑋 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } ) )
7	6	simprbi	⊢ ( 𝑋 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } )
8	3 7	syl6bi	⊢ ( 𝑉 ∈ V → ( 𝑋 ∈ ( Pairs ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } ) )
9	1 8	mpcom	⊢ ( 𝑋 ∈ ( Pairs ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } )