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

Metamath Proof Explorer

Theorem opreuopreu

Description: There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023)

Ref Expression
Hypothesis opreuopreu.a 
|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ps <-> ph ) )
Assertion opreuopreu 
|- ( E! p e. ( A X. B ) ph <-> E! p e. ( A X. B ) E. a E. b ( p = <. a , b >. /\ ps ) )

Proof

Step Hyp Ref Expression
1 opreuopreu.a 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ps <-> ph ) )
2 elxpi 
 |-  ( p e. ( A X. B ) -> E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) )
3 simprl 
 |-  ( ( ph /\ ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) ) -> p = <. a , b >. )
4 vex 
 |-  a e. _V
5 vex 
 |-  b e. _V
6 4 5 op1st 
 |-  ( 1st ` <. a , b >. ) = a
7 6 eqcomi 
 |-  a = ( 1st ` <. a , b >. )
8 4 5 op2nd 
 |-  ( 2nd ` <. a , b >. ) = b
9 8 eqcomi 
 |-  b = ( 2nd ` <. a , b >. )
10 7 9 pm3.2i 
 |-  ( a = ( 1st ` <. a , b >. ) /\ b = ( 2nd ` <. a , b >. ) )
11 fveq2 
 |-  ( p = <. a , b >. -> ( 1st ` p ) = ( 1st ` <. a , b >. ) )
12 11 eqeq2d 
 |-  ( p = <. a , b >. -> ( a = ( 1st ` p ) <-> a = ( 1st ` <. a , b >. ) ) )
13 fveq2 
 |-  ( p = <. a , b >. -> ( 2nd ` p ) = ( 2nd ` <. a , b >. ) )
14 13 eqeq2d 
 |-  ( p = <. a , b >. -> ( b = ( 2nd ` p ) <-> b = ( 2nd ` <. a , b >. ) ) )
15 12 14 anbi12d 
 |-  ( p = <. a , b >. -> ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) <-> ( a = ( 1st ` <. a , b >. ) /\ b = ( 2nd ` <. a , b >. ) ) ) )
16 10 15 mpbiri 
 |-  ( p = <. a , b >. -> ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) )
17 16 1 syl 
 |-  ( p = <. a , b >. -> ( ps <-> ph ) )
18 17 biimprd 
 |-  ( p = <. a , b >. -> ( ph -> ps ) )
19 18 adantr 
 |-  ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ph -> ps ) )
20 19 impcom 
 |-  ( ( ph /\ ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) ) -> ps )
21 3 20 jca 
 |-  ( ( ph /\ ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) ) -> ( p = <. a , b >. /\ ps ) )
22 21 ex 
 |-  ( ph -> ( ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( p = <. a , b >. /\ ps ) ) )
23 22 2eximdv 
 |-  ( ph -> ( E. a E. b ( p = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> E. a E. b ( p = <. a , b >. /\ ps ) ) )
24 2 23 syl5com 
 |-  ( p e. ( A X. B ) -> ( ph -> E. a E. b ( p = <. a , b >. /\ ps ) ) )
25 17 biimpa 
 |-  ( ( p = <. a , b >. /\ ps ) -> ph )
26 25 a1i 
 |-  ( p e. ( A X. B ) -> ( ( p = <. a , b >. /\ ps ) -> ph ) )
27 26 exlimdvv 
 |-  ( p e. ( A X. B ) -> ( E. a E. b ( p = <. a , b >. /\ ps ) -> ph ) )
28 24 27 impbid 
 |-  ( p e. ( A X. B ) -> ( ph <-> E. a E. b ( p = <. a , b >. /\ ps ) ) )
29 28 reubiia 
 |-  ( E! p e. ( A X. B ) ph <-> E! p e. ( A X. B ) E. a E. b ( p = <. a , b >. /\ ps ) )