Theorem pr2eldif1

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	pr2eldif1	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to A\in \left(\left\{A,B\right\}\setminus \left\{B\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		prid1g	$$⊢A\in \mathrm{V}\to A\in \left\{A,B\right\}$$
3	2	3ad2ant1	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to A\in \left\{A,B\right\}$$
4		nelsn	$$⊢A\ne B\to \neg A\in \left\{B\right\}$$
5	4	3ad2ant3	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to \neg A\in \left\{B\right\}$$
6	3 5	eldifd	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to A\in \left(\left\{A,B\right\}\setminus \left\{B\right\}\right)$$
7	1 6	sylbi	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to A\in \left(\left\{A,B\right\}\setminus \left\{B\right\}\right)$$