Theorem prsssprel

Description: The elements of a pair from a subset of the set of all unordered pairs over a given set V are elements of the set V . (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	prsssprel	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ { 𝑋 , 𝑌 } ∈ 𝑃 ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		ssel2	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ { 𝑋 , 𝑌 } ∈ 𝑃 ) → { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) )
2		prsprel	⊢ ( ( { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
3	1 2	stoic3	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ { 𝑋 , 𝑌 } ∈ 𝑃 ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )