Theorem prprc1

Description: A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Assertion	prprc1	$$⊢\neg A\in \mathrm{V}\to \left\{A,B\right\}=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
2		uneq1	$$⊢\left\{A\right\}=\varnothing \to \left\{A\right\}\cup \left\{B\right\}=\varnothing \cup \left\{B\right\}$$
3		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
4		uncom	$$⊢\varnothing \cup \left\{B\right\}=\left\{B\right\}\cup \varnothing$$
5		un0	$$⊢\left\{B\right\}\cup \varnothing =\left\{B\right\}$$
6	4 5	eqtr2i	$$⊢\left\{B\right\}=\varnothing \cup \left\{B\right\}$$
7	2 3 6	3eqtr4g	$$⊢\left\{A\right\}=\varnothing \to \left\{A,B\right\}=\left\{B\right\}$$
8	1 7	sylbi	$$⊢\neg A\in \mathrm{V}\to \left\{A,B\right\}=\left\{B\right\}$$