Theorem pr2eldif2

Description: If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023)

	Ref	Expression
Assertion	pr2eldif2	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to B\in \left(\left\{A,B\right\}\setminus \left\{A\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pren2	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)$$
2		prid2g	$$⊢B\in \mathrm{V}\to B\in \left\{A,B\right\}$$
3	2	3ad2ant2	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to B\in \left\{A,B\right\}$$
4		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
5		nelsn	$$⊢B\ne A\to \neg B\in \left\{A\right\}$$
6	4 5	sylbi	$$⊢A\ne B\to \neg B\in \left\{A\right\}$$
7	6	3ad2ant3	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to \neg B\in \left\{A\right\}$$
8	3 7	eldifd	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to B\in \left(\left\{A,B\right\}\setminus \left\{A\right\}\right)$$
9	1 8	sylbi	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to B\in \left(\left\{A,B\right\}\setminus \left\{A\right\}\right)$$