Metamath Proof Explorer

Theorem reuprg0

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

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

Proof

Step Hyp Ref Expression
1 reuprg.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 reuprg.2 
 |-  ( x = B -> ( ph <-> ch ) )
3 nfsbc1v 
 |-  F/ x [. c / x ]. ph
4 nfsbc1v 
 |-  F/ x [. w / x ]. ph
5 sbceq1a 
 |-  ( x = w -> ( ph <-> [. w / x ]. ph ) )
6 dfsbcq 
 |-  ( w = c -> ( [. w / x ]. ph <-> [. c / x ]. ph ) )
7 3 4 5 6 reu8nf 
 |-  ( E! x e. { A , B } ph <-> E. x e. { A , B } ( ph /\ A. c e. { A , B } ( [. c / x ]. ph -> x = c ) ) )
8 nfv 
 |-  F/ x ps
9 nfcv 
 |-  F/_ x { A , B }
10 nfv 
 |-  F/ x A = c
11 3 10 nfim 
 |-  F/ x ( [. c / x ]. ph -> A = c )
12 9 11 nfralw 
 |-  F/ x A. c e. { A , B } ( [. c / x ]. ph -> A = c )
13 8 12 nfan 
 |-  F/ x ( ps /\ A. c e. { A , B } ( [. c / x ]. ph -> A = c ) )
14 nfv 
 |-  F/ x ch
15 nfv 
 |-  F/ x B = c
16 3 15 nfim 
 |-  F/ x ( [. c / x ]. ph -> B = c )
17 9 16 nfralw 
 |-  F/ x A. c e. { A , B } ( [. c / x ]. ph -> B = c )
18 14 17 nfan 
 |-  F/ x ( ch /\ A. c e. { A , B } ( [. c / x ]. ph -> B = c ) )
19 eqeq1 
 |-  ( x = A -> ( x = c <-> A = c ) )
20 19 imbi2d 
 |-  ( x = A -> ( ( [. c / x ]. ph -> x = c ) <-> ( [. c / x ]. ph -> A = c ) ) )
21 20 ralbidv 
 |-  ( x = A -> ( A. c e. { A , B } ( [. c / x ]. ph -> x = c ) <-> A. c e. { A , B } ( [. c / x ]. ph -> A = c ) ) )
22 1 21 anbi12d 
 |-  ( x = A -> ( ( ph /\ A. c e. { A , B } ( [. c / x ]. ph -> x = c ) ) <-> ( ps /\ A. c e. { A , B } ( [. c / x ]. ph -> A = c ) ) ) )
23 eqeq1 
 |-  ( x = B -> ( x = c <-> B = c ) )
24 23 imbi2d 
 |-  ( x = B -> ( ( [. c / x ]. ph -> x = c ) <-> ( [. c / x ]. ph -> B = c ) ) )
25 24 ralbidv 
 |-  ( x = B -> ( A. c e. { A , B } ( [. c / x ]. ph -> x = c ) <-> A. c e. { A , B } ( [. c / x ]. ph -> B = c ) ) )
26 2 25 anbi12d 
 |-  ( x = B -> ( ( ph /\ A. c e. { A , B } ( [. c / x ]. ph -> x = c ) ) <-> ( ch /\ A. c e. { A , B } ( [. c / x ]. ph -> B = c ) ) ) )
27 13 18 22 26 rexprgf 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ( ph /\ A. c e. { A , B } ( [. c / x ]. ph -> x = c ) ) <-> ( ( ps /\ A. c e. { A , B } ( [. c / x ]. ph -> A = c ) ) \/ ( ch /\ A. c e. { A , B } ( [. c / x ]. ph -> B = c ) ) ) ) )
28 dfsbcq 
 |-  ( c = A -> ( [. c / x ]. ph <-> [. A / x ]. ph ) )
29 eqeq2 
 |-  ( c = A -> ( A = c <-> A = A ) )
30 28 29 imbi12d 
 |-  ( c = A -> ( ( [. c / x ]. ph -> A = c ) <-> ( [. A / x ]. ph -> A = A ) ) )
31 dfsbcq 
 |-  ( c = B -> ( [. c / x ]. ph <-> [. B / x ]. ph ) )
32 eqeq2 
 |-  ( c = B -> ( A = c <-> A = B ) )
33 31 32 imbi12d 
 |-  ( c = B -> ( ( [. c / x ]. ph -> A = c ) <-> ( [. B / x ]. ph -> A = B ) ) )
34 30 33 ralprg 
 |-  ( ( A e. V /\ B e. W ) -> ( A. c e. { A , B } ( [. c / x ]. ph -> A = c ) <-> ( ( [. A / x ]. ph -> A = A ) /\ ( [. B / x ]. ph -> A = B ) ) ) )
35 eqidd 
 |-  ( [. A / x ]. ph -> A = A )
36 35 biantrur 
 |-  ( ( [. B / x ]. ph -> A = B ) <-> ( ( [. A / x ]. ph -> A = A ) /\ ( [. B / x ]. ph -> A = B ) ) )
37 2 sbcieg 
 |-  ( B e. W -> ( [. B / x ]. ph <-> ch ) )
38 37 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ( [. B / x ]. ph <-> ch ) )
39 38 imbi1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [. B / x ]. ph -> A = B ) <-> ( ch -> A = B ) ) )
40 36 39 bitr3id 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ( [. A / x ]. ph -> A = A ) /\ ( [. B / x ]. ph -> A = B ) ) <-> ( ch -> A = B ) ) )
41 34 40 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( A. c e. { A , B } ( [. c / x ]. ph -> A = c ) <-> ( ch -> A = B ) ) )
42 41 anbi2d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ps /\ A. c e. { A , B } ( [. c / x ]. ph -> A = c ) ) <-> ( ps /\ ( ch -> A = B ) ) ) )
43 eqeq2 
 |-  ( c = A -> ( B = c <-> B = A ) )
44 28 43 imbi12d 
 |-  ( c = A -> ( ( [. c / x ]. ph -> B = c ) <-> ( [. A / x ]. ph -> B = A ) ) )
45 eqeq2 
 |-  ( c = B -> ( B = c <-> B = B ) )
46 31 45 imbi12d 
 |-  ( c = B -> ( ( [. c / x ]. ph -> B = c ) <-> ( [. B / x ]. ph -> B = B ) ) )
47 44 46 ralprg 
 |-  ( ( A e. V /\ B e. W ) -> ( A. c e. { A , B } ( [. c / x ]. ph -> B = c ) <-> ( ( [. A / x ]. ph -> B = A ) /\ ( [. B / x ]. ph -> B = B ) ) ) )
48 eqidd 
 |-  ( [. B / x ]. ph -> B = B )
49 48 biantru 
 |-  ( ( [. A / x ]. ph -> B = A ) <-> ( ( [. A / x ]. ph -> B = A ) /\ ( [. B / x ]. ph -> B = B ) ) )
50 1 sbcieg 
 |-  ( A e. V -> ( [. A / x ]. ph <-> ps ) )
51 50 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ( [. A / x ]. ph <-> ps ) )
52 51 imbi1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [. A / x ]. ph -> B = A ) <-> ( ps -> B = A ) ) )
53 49 52 bitr3id 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ( [. A / x ]. ph -> B = A ) /\ ( [. B / x ]. ph -> B = B ) ) <-> ( ps -> B = A ) ) )
54 47 53 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( A. c e. { A , B } ( [. c / x ]. ph -> B = c ) <-> ( ps -> B = A ) ) )
55 54 anbi2d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ch /\ A. c e. { A , B } ( [. c / x ]. ph -> B = c ) ) <-> ( ch /\ ( ps -> B = A ) ) ) )
56 eqcom 
 |-  ( B = A <-> A = B )
57 56 imbi2i 
 |-  ( ( ps -> B = A ) <-> ( ps -> A = B ) )
58 57 anbi2i 
 |-  ( ( ch /\ ( ps -> B = A ) ) <-> ( ch /\ ( ps -> A = B ) ) )
59 55 58 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ch /\ A. c e. { A , B } ( [. c / x ]. ph -> B = c ) ) <-> ( ch /\ ( ps -> A = B ) ) ) )
60 42 59 orbi12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ( ps /\ A. c e. { A , B } ( [. c / x ]. ph -> A = c ) ) \/ ( ch /\ A. c e. { A , B } ( [. c / x ]. ph -> B = c ) ) ) <-> ( ( ps /\ ( ch -> A = B ) ) \/ ( ch /\ ( ps -> A = B ) ) ) ) )
61 27 60 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ( ph /\ A. c e. { A , B } ( [. c / x ]. ph -> x = c ) ) <-> ( ( ps /\ ( ch -> A = B ) ) \/ ( ch /\ ( ps -> A = B ) ) ) ) )
62 7 61 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( E! x e. { A , B } ph <-> ( ( ps /\ ( ch -> A = B ) ) \/ ( ch /\ ( ps -> A = B ) ) ) ) )