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

Metamath Proof Explorer

Theorem opreu2reurex

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

Ref Expression
Hypothesis opreu2reurex.a 
|- ( p = <. a , b >. -> ( ph <-> ch ) )
Assertion opreu2reurex 
|- ( E! p e. ( A X. B ) ph <-> ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) )

Proof

Step Hyp Ref Expression
1 opreu2reurex.a 
 |-  ( p = <. a , b >. -> ( ph <-> ch ) )
2 eqcom 
 |-  ( <. x , y >. = <. a , b >. <-> <. a , b >. = <. x , y >. )
3 vex 
 |-  a e. _V
4 vex 
 |-  b e. _V
5 3 4 opth 
 |-  ( <. a , b >. = <. x , y >. <-> ( a = x /\ b = y ) )
6 2 5 bitri 
 |-  ( <. x , y >. = <. a , b >. <-> ( a = x /\ b = y ) )
7 6 imbi2i 
 |-  ( ( ch -> <. x , y >. = <. a , b >. ) <-> ( ch -> ( a = x /\ b = y ) ) )
8 7 a1i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( a e. A /\ b e. B ) ) -> ( ( ch -> <. x , y >. = <. a , b >. ) <-> ( ch -> ( a = x /\ b = y ) ) ) )
9 8 2ralbidva 
 |-  ( ( x e. A /\ y e. B ) -> ( A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) <-> A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
10 9 2rexbiia 
 |-  ( E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) <-> E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) )
11 10 anbi2i 
 |-  ( ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) ) <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
12 1 reu3op 
 |-  ( E! p e. ( A X. B ) ph <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> <. x , y >. = <. a , b >. ) ) )
13 2reu4 
 |-  ( ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
14 11 12 13 3bitr4i 
 |-  ( E! p e. ( A X. B ) ph <-> ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) )