Theorem tpprceq3

Description: An unordered triple is an unordered pair if one of its elements is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ianor	$$⊢\neg \left(C\in \mathrm{V}\wedge C\ne B\right)\leftrightarrow \left(\neg C\in \mathrm{V}\vee \neg C\ne B\right)$$
2		prprc2	$$⊢\neg C\in \mathrm{V}\to \left\{B,C\right\}=\left\{B\right\}$$
3	2	uneq1d	$$⊢\neg C\in \mathrm{V}\to \left\{B,C\right\}\cup \left\{A\right\}=\left\{B\right\}\cup \left\{A\right\}$$
4		tprot	$$⊢\left\{A,B,C\right\}=\left\{B,C,A\right\}$$
5		df-tp	$$⊢\left\{B,C,A\right\}=\left\{B,C\right\}\cup \left\{A\right\}$$
6	4 5	eqtri	$$⊢\left\{A,B,C\right\}=\left\{B,C\right\}\cup \left\{A\right\}$$
7		prcom	$$⊢\left\{A,B\right\}=\left\{B,A\right\}$$
8		df-pr	$$⊢\left\{B,A\right\}=\left\{B\right\}\cup \left\{A\right\}$$
9	7 8	eqtri	$$⊢\left\{A,B\right\}=\left\{B\right\}\cup \left\{A\right\}$$
10	3 6 9	3eqtr4g	$$⊢\neg C\in \mathrm{V}\to \left\{A,B,C\right\}=\left\{A,B\right\}$$
11		nne	$$⊢\neg C\ne B\leftrightarrow C=B$$
12		tppreq3	$$⊢B=C\to \left\{A,B,C\right\}=\left\{A,B\right\}$$
13	12	eqcoms	$$⊢C=B\to \left\{A,B,C\right\}=\left\{A,B\right\}$$
14	11 13	sylbi	$$⊢\neg C\ne B\to \left\{A,B,C\right\}=\left\{A,B\right\}$$
15	10 14	jaoi	$$⊢\left(\neg C\in \mathrm{V}\vee \neg C\ne B\right)\to \left\{A,B,C\right\}=\left\{A,B\right\}$$
16	1 15	sylbi	$$⊢\neg \left(C\in \mathrm{V}\wedge C\ne B\right)\to \left\{A,B,C\right\}=\left\{A,B\right\}$$