Theorem pr2ne

Description: If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 30-Dec-2024)

	Ref	Expression
Assertion	pr2ne	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow A\ne B\right)$$

Proof

Step	Hyp	Ref	Expression
1		snnen2o	$$⊢\neg \left\{A\right\}\approx 2_{𝑜}$$
2		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
3		preq2	$$⊢A=B\to \left\{A,A\right\}=\left\{A,B\right\}$$
4	2 3	eqtr2id	$$⊢A=B\to \left\{A,B\right\}=\left\{A\right\}$$
5	4	breq1d	$$⊢A=B\to \left(\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow \left\{A\right\}\approx 2_{𝑜}\right)$$
6	1 5	mtbiri	$$⊢A=B\to \neg \left\{A,B\right\}\approx 2_{𝑜}$$
7	6	necon2ai	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to A\ne B$$
8		enpr2	$$⊢\left(A\in C\wedge B\in D\wedge A\ne B\right)\to \left\{A,B\right\}\approx 2_{𝑜}$$
9	8	3expia	$$⊢\left(A\in C\wedge B\in D\right)\to \left(A\ne B\to \left\{A,B\right\}\approx 2_{𝑜}\right)$$
10	7 9	impbid2	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow A\ne B\right)$$