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 preq2 
 |-  ( b = Y -> { A , b } = { A , Y } )
3 2 eqeq2d 
 |-  ( b = Y -> ( { X , Y } = { A , b } <-> { X , Y } = { A , Y } ) )
4 3 adantl 
 |-  ( ( ( A = X /\ ( X e. V /\ Y e. V ) ) /\ b = Y ) -> ( { X , Y } = { A , b } <-> { X , Y } = { A , Y } ) )
5 preq1 
 |-  ( X = A -> { X , Y } = { A , Y } )
6 5 eqcoms 
 |-  ( A = X -> { X , Y } = { A , Y } )
7 6 adantr 
 |-  ( ( A = X /\ ( X e. V /\ Y e. V ) ) -> { X , Y } = { A , Y } )
8 1 4 7 rspcedvd 
 |-  ( ( A = X /\ ( X e. V /\ Y e. V ) ) -> E. b e. V { X , Y } = { A , b } )
9 8 ex 
 |-  ( A = X -> ( ( X e. V /\ Y e. V ) -> E. b e. V { X , Y } = { A , b } ) )
10 simprl 
 |-  ( ( A = Y /\ ( X e. V /\ Y e. V ) ) -> X e. V )
11 preq2 
 |-  ( b = X -> { A , b } = { A , X } )
12 11 eqeq2d 
 |-  ( b = X -> ( { X , Y } = { A , b } <-> { X , Y } = { A , X } ) )
13 12 adantl 
 |-  ( ( ( A = Y /\ ( X e. V /\ Y e. V ) ) /\ b = X ) -> ( { X , Y } = { A , b } <-> { X , Y } = { A , X } ) )
14 preq2 
 |-  ( Y = A -> { X , Y } = { X , A } )
15 14 eqcoms 
 |-  ( A = Y -> { X , Y } = { X , A } )
16 prcom 
 |-  { X , A } = { A , X }
17 15 16 eqtrdi 
 |-  ( A = Y -> { X , Y } = { A , X } )
18 17 adantr 
 |-  ( ( A = Y /\ ( X e. V /\ Y e. V ) ) -> { X , Y } = { A , X } )
19 10 13 18 rspcedvd 
 |-  ( ( A = Y /\ ( X e. V /\ Y e. V ) ) -> E. b e. V { X , Y } = { A , b } )
20 19 ex 
 |-  ( A = Y -> ( ( X e. V /\ Y e. V ) -> E. b e. V { X , Y } = { A , b } ) )
21 9 20 jaoi 
 |-  ( ( A = X \/ A = Y ) -> ( ( X e. V /\ Y e. V ) -> E. b e. V { X , Y } = { A , b } ) )
22 elpri 
 |-  ( A e. { X , Y } -> ( A = X \/ A = Y ) )
23 21 22 syl11 
 |-  ( ( X e. V /\ Y e. V ) -> ( A e. { X , Y } -> E. b e. V { X , Y } = { A , b } ) )
24 23 3impia 
 |-  ( ( X e. V /\ Y e. V /\ A e. { X , Y } ) -> E. b e. V { X , Y } = { A , b } )