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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		elpreqpr	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } )
2		prid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝑥 } )
3		eleq2	⊢ ( { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ 𝐴 ∈ { 𝐴 , 𝑥 } ) )
4	2 3	syl5ibrcom	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } → 𝐴 ∈ { 𝐵 , 𝐶 } ) )
5	4	exlimdv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } → 𝐴 ∈ { 𝐵 , 𝐶 } ) )
6	1 5	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } ) )