Theorem sprid

Description: Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	sprid	$$⊢\left\{p|\exists a\in \mathrm{V}\exists b\in \mathrm{V}p=\left\{a,b\right\}\right\}=\left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rexv	$$⊢\exists a\in \mathrm{V}\exists b\in \mathrm{V}p=\left\{a,b\right\}\leftrightarrow \exists a\exists b\in \mathrm{V}p=\left\{a,b\right\}$$
2		rexv	$$⊢\exists b\in \mathrm{V}p=\left\{a,b\right\}\leftrightarrow \exists bp=\left\{a,b\right\}$$
3	2	exbii	$$⊢\exists a\exists b\in \mathrm{V}p=\left\{a,b\right\}\leftrightarrow \exists a\exists bp=\left\{a,b\right\}$$
4	1 3	bitri	$$⊢\exists a\in \mathrm{V}\exists b\in \mathrm{V}p=\left\{a,b\right\}\leftrightarrow \exists a\exists bp=\left\{a,b\right\}$$
5	4	abbii	$$⊢\left\{p|\exists a\in \mathrm{V}\exists b\in \mathrm{V}p=\left\{a,b\right\}\right\}=\left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$