Theorem elpreqprb

Description: A set is an element of an unordered pair iff there is another (maybe the same) set which is an element of the unordered pair. (Proposed by BJ, 8-Dec-2020.) (Contributed by AV, 9-Dec-2020)

	Ref	Expression
Assertion	elpreqprb	$$⊢A\in V\to \left(A\in \left\{B,C\right\}\leftrightarrow \exists x\left\{B,C\right\}=\left\{A,x\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpreqpr	$$⊢A\in \left\{B,C\right\}\to \exists x\left\{B,C\right\}=\left\{A,x\right\}$$
2		prid1g	$$⊢A\in V\to A\in \left\{A,x\right\}$$
3		eleq2	$$⊢\left\{B,C\right\}=\left\{A,x\right\}\to \left(A\in \left\{B,C\right\}\leftrightarrow A\in \left\{A,x\right\}\right)$$
4	2 3	syl5ibrcom	$$⊢A\in V\to \left(\left\{B,C\right\}=\left\{A,x\right\}\to A\in \left\{B,C\right\}\right)$$
5	4	exlimdv	$$⊢A\in V\to \left(\exists x\left\{B,C\right\}=\left\{A,x\right\}\to A\in \left\{B,C\right\}\right)$$
6	1 5	impbid2	$$⊢A\in V\to \left(A\in \left\{B,C\right\}\leftrightarrow \exists x\left\{B,C\right\}=\left\{A,x\right\}\right)$$