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	$$⊢\left(P\subseteq \mathrm{Pairs}\left(V\right)\wedge X\in P\right)\to \exists a\in V\exists b\in VX=\left\{a,b\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssel2	$$⊢\left(P\subseteq \mathrm{Pairs}\left(V\right)\wedge X\in P\right)\to X\in \mathrm{Pairs}\left(V\right)$$
2		sprel	$$⊢X\in \mathrm{Pairs}\left(V\right)\to \exists a\in V\exists b\in VX=\left\{a,b\right\}$$
3	1 2	syl	$$⊢\left(P\subseteq \mathrm{Pairs}\left(V\right)\wedge X\in P\right)\to \exists a\in V\exists b\in VX=\left\{a,b\right\}$$