Metamath Proof Explorer

Theorem reuprg

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

Ref Expression
Hypotheses reuprg.1 
|- ( x = A -> ( ph <-> ps ) )
reuprg.2 
|- ( x = B -> ( ph <-> ch ) )
Assertion reuprg 
|- ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( ( ps \/ ch ) /\ ( ( 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 reuprg0 
 |-  ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( ( ps /\ ( ch -> A = B ) ) \/ ( ch /\ ( ps -> A = B ) ) ) ) )
4 orddi 
 |-  ( ( ( ps /\ ( ch -> A = B ) ) \/ ( ch /\ ( ps -> A = B ) ) ) <-> ( ( ( ps \/ ch ) /\ ( ps \/ ( ps -> A = B ) ) ) /\ ( ( ( ch -> A = B ) \/ ch ) /\ ( ( ch -> A = B ) \/ ( ps -> A = B ) ) ) ) )
5 curryax 
 |-  ( ps \/ ( ps -> A = B ) )
6 5 biantru 
 |-  ( ( ps \/ ch ) <-> ( ( ps \/ ch ) /\ ( ps \/ ( ps -> A = B ) ) ) )
7 6 bicomi 
 |-  ( ( ( ps \/ ch ) /\ ( ps \/ ( ps -> A = B ) ) ) <-> ( ps \/ ch ) )
8 curryax 
 |-  ( ch \/ ( ch -> A = B ) )
9 orcom 
 |-  ( ( ( ch -> A = B ) \/ ch ) <-> ( ch \/ ( ch -> A = B ) ) )
10 8 9 mpbir 
 |-  ( ( ch -> A = B ) \/ ch )
11 10 biantrur 
 |-  ( ( ( ch -> A = B ) \/ ( ps -> A = B ) ) <-> ( ( ( ch -> A = B ) \/ ch ) /\ ( ( ch -> A = B ) \/ ( ps -> A = B ) ) ) )
12 11 bicomi 
 |-  ( ( ( ( ch -> A = B ) \/ ch ) /\ ( ( ch -> A = B ) \/ ( ps -> A = B ) ) ) <-> ( ( ch -> A = B ) \/ ( ps -> A = B ) ) )
13 pm4.79 
 |-  ( ( ( ch -> A = B ) \/ ( ps -> A = B ) ) <-> ( ( ch /\ ps ) -> A = B ) )
14 12 13 bitri 
 |-  ( ( ( ( ch -> A = B ) \/ ch ) /\ ( ( ch -> A = B ) \/ ( ps -> A = B ) ) ) <-> ( ( ch /\ ps ) -> A = B ) )
15 7 14 anbi12i 
 |-  ( ( ( ( ps \/ ch ) /\ ( ps \/ ( ps -> A = B ) ) ) /\ ( ( ( ch -> A = B ) \/ ch ) /\ ( ( ch -> A = B ) \/ ( ps -> A = B ) ) ) ) <-> ( ( ps \/ ch ) /\ ( ( ch /\ ps ) -> A = B ) ) )
16 4 15 bitri 
 |-  ( ( ( ps /\ ( ch -> A = B ) ) \/ ( ch /\ ( ps -> A = B ) ) ) <-> ( ( ps \/ ch ) /\ ( ( ch /\ ps ) -> A = B ) ) )
17 3 16 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( ( ps \/ ch ) /\ ( ( ch /\ ps ) -> A = B ) ) ) )