Theorem hash2sspr

Description: A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017) (Proof shortened by AV, 4-Nov-2020)

	Ref	Expression
Assertion	hash2sspr	$$⊢\left(P\in 𝒫V\wedge \left|P\right|=2\right)\to \exists a\in V\exists b\in VP=\left\{a,b\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢p=P\to \left(\left|p\right|=2\leftrightarrow \left|P\right|=2\right)$$
2	1	elrab	$$⊢P\in \left\{p\in 𝒫V|\left|p\right|=2\right\}\leftrightarrow \left(P\in 𝒫V\wedge \left|P\right|=2\right)$$
3		elss2prb	$$⊢P\in \left\{p\in 𝒫V|\left|p\right|=2\right\}\leftrightarrow \exists a\in V\exists b\in V\left(a\ne b\wedge P=\left\{a,b\right\}\right)$$
4		simpr	$$⊢\left(a\ne b\wedge P=\left\{a,b\right\}\right)\to P=\left\{a,b\right\}$$
5	4	reximi	$$⊢\exists b\in V\left(a\ne b\wedge P=\left\{a,b\right\}\right)\to \exists b\in VP=\left\{a,b\right\}$$
6	5	reximi	$$⊢\exists a\in V\exists b\in V\left(a\ne b\wedge P=\left\{a,b\right\}\right)\to \exists a\in V\exists b\in VP=\left\{a,b\right\}$$
7	3 6	sylbi	$$⊢P\in \left\{p\in 𝒫V|\left|p\right|=2\right\}\to \exists a\in V\exists b\in VP=\left\{a,b\right\}$$
8	2 7	sylbir	$$⊢\left(P\in 𝒫V\wedge \left|P\right|=2\right)\to \exists a\in V\exists b\in VP=\left\{a,b\right\}$$