Theorem prssspr

Description: An element of a subset 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	prssspr	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } )

Proof

Step	Hyp	Ref	Expression
1		ssel2	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ∈ ( Pairs ‘ 𝑉 ) )
2		sprel	⊢ ( 𝑋 ∈ ( Pairs ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } )
3	1 2	syl	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑋 = { 𝑎 , 𝑏 } )