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

Proof

Step	Hyp	Ref	Expression
1		elfvex	$$⊢X\in \mathrm{Pairs}\left(V\right)\to V\in \mathrm{V}$$
2		sprvalpw	$$⊢V\in \mathrm{V}\to \mathrm{Pairs}\left(V\right)=\left\{p\in 𝒫V|\exists a\in V\exists b\in Vp=\left\{a,b\right\}\right\}$$
3	2	eleq2d	$$⊢V\in \mathrm{V}\to \left(X\in \mathrm{Pairs}\left(V\right)\leftrightarrow X\in \left\{p\in 𝒫V|\exists a\in V\exists b\in Vp=\left\{a,b\right\}\right\}\right)$$
4		eqeq1	$$⊢p=X\to \left(p=\left\{a,b\right\}\leftrightarrow X=\left\{a,b\right\}\right)$$
5	4	2rexbidv	$$⊢p=X\to \left(\exists a\in V\exists b\in Vp=\left\{a,b\right\}\leftrightarrow \exists a\in V\exists b\in VX=\left\{a,b\right\}\right)$$
6	5	elrab	$$⊢X\in \left\{p\in 𝒫V|\exists a\in V\exists b\in Vp=\left\{a,b\right\}\right\}\leftrightarrow \left(X\in 𝒫V\wedge \exists a\in V\exists b\in VX=\left\{a,b\right\}\right)$$
7	6	simprbi	$$⊢X\in \left\{p\in 𝒫V|\exists a\in V\exists b\in Vp=\left\{a,b\right\}\right\}\to \exists a\in V\exists b\in VX=\left\{a,b\right\}$$
8	3 7	syl6bi	$$⊢V\in \mathrm{V}\to \left(X\in \mathrm{Pairs}\left(V\right)\to \exists a\in V\exists b\in VX=\left\{a,b\right\}\right)$$
9	1 8	mpcom	$$⊢X\in \mathrm{Pairs}\left(V\right)\to \exists a\in V\exists b\in VX=\left\{a,b\right\}$$