This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )