Theorem elpr2elpr

Description: For an element A of an unordered pair which is a subset of a given set V , there is another (maybe the same) element b of the given set V being an element of the unordered pair. (Contributed by AV, 5-Dec-2020)

	Ref	Expression
Assertion	elpr2elpr	|- ( ( X e. V /\ Y e. V /\ A e. { X , Y } ) -> E. b e. V { X , Y } = { A , b } )

Proof

Step	Hyp	Ref	Expression
1		simprr	|- ( ( A = X /\ ( X e. V /\ Y e. V ) ) -> Y e. V )
2		preq12	|- ( ( A = X /\ b = Y ) -> { A , b } = { X , Y } )
3	2	eqcomd	|- ( ( A = X /\ b = Y ) -> { X , Y } = { A , b } )
4	3	adantlr	|- ( ( ( A = X /\ ( X e. V /\ Y e. V ) ) /\ b = Y ) -> { X , Y } = { A , b } )
5	1 4	rspcedeq2vd	|- ( ( A = X /\ ( X e. V /\ Y e. V ) ) -> E. b e. V { X , Y } = { A , b } )
6	5	ex	|- ( A = X -> ( ( X e. V /\ Y e. V ) -> E. b e. V { X , Y } = { A , b } ) )
7		simprl	|- ( ( A = Y /\ ( X e. V /\ Y e. V ) ) -> X e. V )
8		preq12	|- ( ( A = Y /\ b = X ) -> { A , b } = { Y , X } )
9		prcom	|- { Y , X } = { X , Y }
10	8 9	eqtr2di	|- ( ( A = Y /\ b = X ) -> { X , Y } = { A , b } )
11	10	adantlr	|- ( ( ( A = Y /\ ( X e. V /\ Y e. V ) ) /\ b = X ) -> { X , Y } = { A , b } )
12	7 11	rspcedeq2vd	|- ( ( A = Y /\ ( X e. V /\ Y e. V ) ) -> E. b e. V { X , Y } = { A , b } )
13	12	ex	|- ( A = Y -> ( ( X e. V /\ Y e. V ) -> E. b e. V { X , Y } = { A , b } ) )
14	6 13	jaoi	|- ( ( A = X \/ A = Y ) -> ( ( X e. V /\ Y e. V ) -> E. b e. V { X , Y } = { A , b } ) )
15		elpri	|- ( A e. { X , Y } -> ( A = X \/ A = Y ) )
16	14 15	syl11	|- ( ( X e. V /\ Y e. V ) -> ( A e. { X , Y } -> E. b e. V { X , Y } = { A , b } ) )
17	16	3impia	|- ( ( X e. V /\ Y e. V /\ A e. { X , Y } ) -> E. b e. V { X , Y } = { A , b } )