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 e. V -> ( A e. { B , C } <-> E. x { B , C } = { A , x } ) )

Proof

Step	Hyp	Ref	Expression
1		elpreqpr	|- ( A e. { B , C } -> E. x { B , C } = { A , x } )
2		prid1g	|- ( A e. V -> A e. { A , x } )
3		eleq2	|- ( { B , C } = { A , x } -> ( A e. { B , C } <-> A e. { A , x } ) )
4	2 3	syl5ibrcom	|- ( A e. V -> ( { B , C } = { A , x } -> A e. { B , C } ) )
5	4	exlimdv	|- ( A e. V -> ( E. x { B , C } = { A , x } -> A e. { B , C } ) )
6	1 5	impbid2	|- ( A e. V -> ( A e. { B , C } <-> E. x { B , C } = { A , x } ) )