Metamath Proof Explorer

Theorem 2reuimp

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (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 2reuimp 
|- ( ( V =/= (/) /\ 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 E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ 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 r19.28zv 
 |-  ( V =/= (/) -> ( A. c e. V ( ch /\ ( ta -> b = c ) ) <-> ( ch /\ A. c e. V ( ta -> b = c ) ) ) )
7 6 bicomd 
 |-  ( V =/= (/) -> ( ( ch /\ A. c e. V ( ta -> b = c ) ) <-> A. c e. V ( ch /\ ( ta -> b = c ) ) ) )
8 7 imbi1d 
 |-  ( V =/= (/) -> ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) <-> ( A. c e. V ( ch /\ ( ta -> b = c ) ) -> a = d ) ) )
9 r19.36zv 
 |-  ( V =/= (/) -> ( E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> a = d ) <-> ( A. c e. V ( ch /\ ( ta -> b = c ) ) -> a = d ) ) )
10 r19.42v 
 |-  ( E. c e. V ( ( et /\ ( ps -> e = f ) ) /\ ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) <-> ( ( et /\ ( ps -> e = f ) ) /\ E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) )
11 pm5.31r 
 |-  ( ( et /\ ( ps -> e = f ) ) -> ( ps -> ( et /\ e = f ) ) )
12 pm5.31r 
 |-  ( ( ( ps -> ( et /\ e = f ) ) /\ ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) -> ( ( ch /\ ( ta -> b = c ) ) -> ( ( ps -> ( et /\ e = f ) ) /\ a = d ) ) )
13 pm5.31r 
 |-  ( ( a = d /\ ( ps -> ( et /\ e = f ) ) ) -> ( ps -> ( a = d /\ ( et /\ e = f ) ) ) )
14 an12 
 |-  ( ( a = d /\ ( et /\ e = f ) ) <-> ( et /\ ( a = d /\ e = f ) ) )
15 13 14 imbitrdi 
 |-  ( ( a = d /\ ( ps -> ( et /\ e = f ) ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) )
16 15 ancoms 
 |-  ( ( ( ps -> ( et /\ e = f ) ) /\ a = d ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) )
17 12 16 syl6 
 |-  ( ( ( ps -> ( et /\ e = f ) ) /\ ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) -> ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) )
18 11 17 sylan 
 |-  ( ( ( et /\ ( ps -> e = f ) ) /\ ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) -> ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) )
19 18 reximi 
 |-  ( E. c e. V ( ( et /\ ( ps -> e = f ) ) /\ ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) )
20 10 19 sylbir 
 |-  ( ( ( et /\ ( ps -> e = f ) ) /\ E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> a = d ) ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) )
21 20 expcom 
 |-  ( E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> a = d ) -> ( ( et /\ ( ps -> e = f ) ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
22 21 expd 
 |-  ( E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> a = d ) -> ( et -> ( ( ps -> e = f ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) ) )
23 9 22 biimtrrdi 
 |-  ( V =/= (/) -> ( ( A. c e. V ( ch /\ ( ta -> b = c ) ) -> a = d ) -> ( et -> ( ( ps -> e = f ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) ) ) )
24 8 23 sylbid 
 |-  ( V =/= (/) -> ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> ( et -> ( ( ps -> e = f ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) ) ) )
25 24 com23 
 |-  ( V =/= (/) -> ( et -> ( ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) -> ( ( ps -> e = f ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) ) ) )
26 25 imp4c 
 |-  ( V =/= (/) -> ( ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) -> E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
27 26 ralimdv 
 |-  ( V =/= (/) -> ( A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) -> A. f e. V E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
28 27 reximdv 
 |-  ( V =/= (/) -> ( E. e e. V A. f e. V ( ( et /\ ( ( ch /\ A. c e. V ( ta -> b = c ) ) -> a = d ) ) /\ ( ps -> e = f ) ) -> E. e e. V A. f e. V E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
29 28 ralimdv 
 |-  ( 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 ) ) -> A. b e. V E. e e. V A. f e. V E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
30 29 ralimdv 
 |-  ( 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 ) ) -> A. d e. V A. b e. V E. e e. V A. f e. V E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
31 30 reximdv 
 |-  ( V =/= (/) -> ( 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 ) ) -> E. a e. V A. d e. V A. b e. V E. e e. V A. f e. V E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) ) )
32 1 2 3 4 5 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 ) ) )
33 31 32 impel 
 |-  ( ( V =/= (/) /\ 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 E. c e. V ( ( ch /\ ( ta -> b = c ) ) -> ( ps -> ( et /\ ( a = d /\ e = f ) ) ) ) )