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

Metamath Proof Explorer

Theorem reurexprg

Description: Convert a restricted existential uniqueness over a pair to a restricted existential quantification and an implication . (Contributed by AV, 3-Apr-2023)

Ref Expression
Hypotheses reuprg.1 
|- ( x = A -> ( ph <-> ps ) )
reuprg.2 
|- ( x = B -> ( ph <-> ch ) )
Assertion reurexprg 
|- ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( E. x e. { A , B } ph /\ ( ( ch /\ ps ) -> A = B ) ) ) )

Proof

Step Hyp Ref Expression
1 reuprg.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 reuprg.2 
 |-  ( x = B -> ( ph <-> ch ) )
3 1 2 reuprg 
 |-  ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( ( ps \/ ch ) /\ ( ( ch /\ ps ) -> A = B ) ) ) )
4 1 2 rexprg 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) )
5 4 bicomd 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ps \/ ch ) <-> E. x e. { A , B } ph ) )
6 5 anbi1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ( ps \/ ch ) /\ ( ( ch /\ ps ) -> A = B ) ) <-> ( E. x e. { A , B } ph /\ ( ( ch /\ ps ) -> A = B ) ) ) )
7 3 6 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( E. x e. { A , B } ph /\ ( ( ch /\ ps ) -> A = B ) ) ) )