Metamath Proof Explorer

Theorem 2reuimp0

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses 2reuimp.c 
|- ( b = c -> ( ph <-> th ) )
2reuimp.d 
|- ( a = d -> ( ph <-> ch ) )
2reuimp.a 
|- ( a = d -> ( th <-> ta ) )
2reuimp.e 
|- ( b = e -> ( ph <-> et ) )
2reuimp.f 
|- ( c = f -> ( th <-> ps ) )
Assertion 2reuimp0 
|- ( E! a e. V E! b e. V ph -> E. a e. V A. d e. V A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )

Proof

Step Hyp Ref Expression
1 2reuimp.c 
 |-  ( b = c -> ( ph <-> th ) )
2 2reuimp.d 
 |-  ( a = d -> ( ph <-> ch ) )
3 2reuimp.a 
 |-  ( a = d -> ( th <-> ta ) )
4 2reuimp.e 
 |-  ( b = e -> ( ph <-> et ) )
5 2reuimp.f 
 |-  ( c = f -> ( th <-> ps ) )
6 1 reu8 
 |-  ( E! b e. V ph <-> E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) )
7 6 reubii 
 |-  ( E! a e. V E! b e. V ph <-> E! a e. V E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) )
8 3 imbi1d 
 |-  ( a = d -> ( ( th -> b = c ) <-> ( ta -> b = c ) ) )
9 8 ralbidv 
 |-  ( a = d -> ( A. c e. V ( th -> b = c ) <-> A. c e. V ( ta -> b = c ) ) )
10 2 9 anbi12d 
 |-  ( a = d -> ( ( ph /\ A. c e. V ( th -> b = c ) ) <-> ( ch /\ A. c e. V ( ta -> b = c ) ) ) )
11 10 rexbidv 
 |-  ( a = d -> ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) <-> E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) ) )
12 11 reu8 
 |-  ( E! a e. V E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) <-> E. a e. V ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ A. d e. V ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) )
13 r19.28v 
 |-  ( ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ A. d e. V ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. d e. V ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) )
14 equequ1 
 |-  ( b = e -> ( b = c <-> e = c ) )
15 14 imbi2d 
 |-  ( b = e -> ( ( th -> b = c ) <-> ( th -> e = c ) ) )
16 15 ralbidv 
 |-  ( b = e -> ( A. c e. V ( th -> b = c ) <-> A. c e. V ( th -> e = c ) ) )
17 4 16 anbi12d 
 |-  ( b = e -> ( ( ph /\ A. c e. V ( th -> b = c ) ) <-> ( et /\ A. c e. V ( th -> e = c ) ) ) )
18 17 cbvrexvw 
 |-  ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) <-> E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) )
19 r19.23v 
 |-  ( A. b e. V ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) <-> ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) )
20 r19.28v 
 |-  ( ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ A. b e. V ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. b e. V ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) )
21 ancom 
 |-  ( ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) <-> ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) /\ E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) ) )
22 r19.42v 
 |-  ( E. e e. V ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) /\ ( et /\ A. c e. V ( th -> e = c ) ) ) <-> ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) /\ E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) ) )
23 21 22 bitr4i 
 |-  ( ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) <-> E. e e. V ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) /\ ( et /\ A. c e. V ( th -> e = c ) ) ) )
24 equequ2 
 |-  ( c = f -> ( e = c <-> e = f ) )
25 5 24 imbi12d 
 |-  ( c = f -> ( ( th -> e = c ) <-> ( ps -> e = f ) ) )
26 25 cbvralvw 
 |-  ( A. c e. V ( th -> e = c ) <-> A. f e. V ( ps -> e = f ) )
27 r19.28v 
 |-  ( ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ A. f e. V ( ps -> e = f ) ) -> A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
28 27 ex 
 |-  ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> ( A. f e. V ( ps -> e = f ) -> A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) ) )
29 28 expcom 
 |-  ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> ( et -> ( A. f e. V ( ps -> e = f ) -> A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) ) ) )
30 26 29 syl7bi 
 |-  ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> ( et -> ( A. c e. V ( th -> e = c ) -> A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) ) ) )
31 30 imp32 
 |-  ( ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) /\ ( et /\ A. c e. V ( th -> e = c ) ) ) -> A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
32 31 reximi 
 |-  ( E. e e. V ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) /\ ( et /\ A. c e. V ( th -> e = c ) ) ) -> E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
33 23 32 sylbi 
 |-  ( ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
34 33 ralimi 
 |-  ( A. b e. V ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
35 20 34 syl 
 |-  ( ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) /\ A. b e. V ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
36 35 ex 
 |-  ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) -> ( A. b e. V ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) ) )
37 19 36 biimtrrid 
 |-  ( E. e e. V ( et /\ A. c e. V ( th -> e = c ) ) -> ( ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) ) )
38 18 37 sylbi 
 |-  ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) -> ( ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) ) )
39 38 imp 
 |-  ( ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
40 39 ralimi 
 |-  ( A. d e. V ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. d e. V A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
41 13 40 syl 
 |-  ( ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ A. d e. V ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> A. d e. V A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
42 41 reximi 
 |-  ( E. a e. V ( E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) /\ A. d e. V ( E. b e. V ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) -> E. a e. V A. d e. V A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
43 12 42 sylbi 
 |-  ( E! a e. V E. b e. V ( ph /\ A. c e. V ( th -> b = c ) ) -> E. a e. V A. d e. V A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )
44 7 43 sylbi 
 |-  ( E! a e. V E! b e. V ph -> E. a e. V A. d e. V A. b e. V E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) )