Theorem prneprprc

Description: A proper unordered pair is not an improper unordered pair. (Contributed by AV, 13-Jun-2022)

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

Proof

Step	Hyp	Ref	Expression
1		prnesn	$$⊢\left(A\in V\wedge B\in W\wedge A\ne B\right)\to \left\{A,B\right\}\ne \left\{D\right\}$$
2	1	adantr	$$⊢\left(\left(A\in V\wedge B\in W\wedge A\ne B\right)\wedge \neg C\in \mathrm{V}\right)\to \left\{A,B\right\}\ne \left\{D\right\}$$
3		prprc1	$$⊢\neg C\in \mathrm{V}\to \left\{C,D\right\}=\left\{D\right\}$$
4	3	neeq2d	$$⊢\neg C\in \mathrm{V}\to \left(\left\{A,B\right\}\ne \left\{C,D\right\}\leftrightarrow \left\{A,B\right\}\ne \left\{D\right\}\right)$$
5	4	adantl	$$⊢\left(\left(A\in V\wedge B\in W\wedge A\ne B\right)\wedge \neg C\in \mathrm{V}\right)\to \left(\left\{A,B\right\}\ne \left\{C,D\right\}\leftrightarrow \left\{A,B\right\}\ne \left\{D\right\}\right)$$
6	2 5	mpbird	$$⊢\left(\left(A\in V\wedge B\in W\wedge A\ne B\right)\wedge \neg C\in \mathrm{V}\right)\to \left\{A,B\right\}\ne \left\{C,D\right\}$$