Theorem prprc

Description: An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006)

	Ref	Expression
Assertion	prprc	$$⊢\left(\neg A\in \mathrm{V}\wedge \neg B\in \mathrm{V}\right)\to \left\{A,B\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		prprc1	$$⊢\neg A\in \mathrm{V}\to \left\{A,B\right\}=\left\{B\right\}$$
2		snprc	$$⊢\neg B\in \mathrm{V}\leftrightarrow \left\{B\right\}=\varnothing$$
3	2	biimpi	$$⊢\neg B\in \mathrm{V}\to \left\{B\right\}=\varnothing$$
4	1 3	sylan9eq	$$⊢\left(\neg A\in \mathrm{V}\wedge \neg B\in \mathrm{V}\right)\to \left\{A,B\right\}=\varnothing$$