Theorem hash2exprb

Description: A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14-Jan-2018)

	Ref	Expression
Assertion	hash2exprb	$$⊢V\in W\to \left(\left|V\right|=2\leftrightarrow \exists a\exists b\left(a\ne b\wedge V=\left\{a,b\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hash2prde	$$⊢\left(V\in W\wedge \left|V\right|=2\right)\to \exists a\exists b\left(a\ne b\wedge V=\left\{a,b\right\}\right)$$
2	1	ex	$$⊢V\in W\to \left(\left|V\right|=2\to \exists a\exists b\left(a\ne b\wedge V=\left\{a,b\right\}\right)\right)$$
3		hashprg	$$⊢\left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\to \left(a\ne b\leftrightarrow \left|\left\{a,b\right\}\right|=2\right)$$
4	3	el2v	$$⊢a\ne b\leftrightarrow \left|\left\{a,b\right\}\right|=2$$
5	4	a1i	$$⊢V=\left\{a,b\right\}\to \left(a\ne b\leftrightarrow \left|\left\{a,b\right\}\right|=2\right)$$
6	5	biimpd	$$⊢V=\left\{a,b\right\}\to \left(a\ne b\to \left|\left\{a,b\right\}\right|=2\right)$$
7		fveqeq2	$$⊢V=\left\{a,b\right\}\to \left(\left|V\right|=2\leftrightarrow \left|\left\{a,b\right\}\right|=2\right)$$
8	6 7	sylibrd	$$⊢V=\left\{a,b\right\}\to \left(a\ne b\to \left|V\right|=2\right)$$
9	8	impcom	$$⊢\left(a\ne b\wedge V=\left\{a,b\right\}\right)\to \left|V\right|=2$$
10	9	a1i	$$⊢V\in W\to \left(\left(a\ne b\wedge V=\left\{a,b\right\}\right)\to \left|V\right|=2\right)$$
11	10	exlimdvv	$$⊢V\in W\to \left(\exists a\exists b\left(a\ne b\wedge V=\left\{a,b\right\}\right)\to \left|V\right|=2\right)$$
12	2 11	impbid	$$⊢V\in W\to \left(\left|V\right|=2\leftrightarrow \exists a\exists b\left(a\ne b\wedge V=\left\{a,b\right\}\right)\right)$$