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

Metamath Proof Explorer

Theorem reu3op

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 1-Jul-2023)

Ref Expression
Hypothesis reu3op.a 
|- ( p = <. a , b >. -> ( ps <-> ch ) )
Assertion reu3op 
|- ( E! p e. ( X X. Y ) ps <-> ( E. a e. X E. b e. Y ch /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )

Proof

Step Hyp Ref Expression
1 reu3op.a 
 |-  ( p = <. a , b >. -> ( ps <-> ch ) )
2 reu3 
 |-  ( E! p e. ( X X. Y ) ps <-> ( E. p e. ( X X. Y ) ps /\ E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) ) )
3 1 rexxp 
 |-  ( E. p e. ( X X. Y ) ps <-> E. a e. X E. b e. Y ch )
4 eqeq2 
 |-  ( q = <. x , y >. -> ( p = q <-> p = <. x , y >. ) )
5 4 imbi2d 
 |-  ( q = <. x , y >. -> ( ( ps -> p = q ) <-> ( ps -> p = <. x , y >. ) ) )
6 5 ralbidv 
 |-  ( q = <. x , y >. -> ( A. p e. ( X X. Y ) ( ps -> p = q ) <-> A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) ) )
7 6 rexxp 
 |-  ( E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) <-> E. x e. X E. y e. Y A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) )
8 eqeq1 
 |-  ( p = <. a , b >. -> ( p = <. x , y >. <-> <. a , b >. = <. x , y >. ) )
9 1 8 imbi12d 
 |-  ( p = <. a , b >. -> ( ( ps -> p = <. x , y >. ) <-> ( ch -> <. a , b >. = <. x , y >. ) ) )
10 9 ralxp 
 |-  ( A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) <-> A. a e. X A. b e. Y ( ch -> <. a , b >. = <. x , y >. ) )
11 eqcom 
 |-  ( <. a , b >. = <. x , y >. <-> <. x , y >. = <. a , b >. )
12 11 a1i 
 |-  ( ( ( x e. X /\ y e. Y ) /\ ( a e. X /\ b e. Y ) ) -> ( <. a , b >. = <. x , y >. <-> <. x , y >. = <. a , b >. ) )
13 12 imbi2d 
 |-  ( ( ( x e. X /\ y e. Y ) /\ ( a e. X /\ b e. Y ) ) -> ( ( ch -> <. a , b >. = <. x , y >. ) <-> ( ch -> <. x , y >. = <. a , b >. ) ) )
14 13 2ralbidva 
 |-  ( ( x e. X /\ y e. Y ) -> ( A. a e. X A. b e. Y ( ch -> <. a , b >. = <. x , y >. ) <-> A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )
15 10 14 bitrid 
 |-  ( ( x e. X /\ y e. Y ) -> ( A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) <-> A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )
16 15 2rexbiia 
 |-  ( E. x e. X E. y e. Y A. p e. ( X X. Y ) ( ps -> p = <. x , y >. ) <-> E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) )
17 7 16 bitri 
 |-  ( E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) <-> E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) )
18 3 17 anbi12i 
 |-  ( ( E. p e. ( X X. Y ) ps /\ E. q e. ( X X. Y ) A. p e. ( X X. Y ) ( ps -> p = q ) ) <-> ( E. a e. X E. b e. Y ch /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )
19 2 18 bitri 
 |-  ( E! p e. ( X X. Y ) ps <-> ( E. a e. X E. b e. Y ch /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) )