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

Metamath Proof Explorer

Theorem reu2eqd

Description: Deduce equality from restricted uniqueness, deduction version. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses reu2eqd.1 
|- ( x = B -> ( ps <-> ch ) )
reu2eqd.2 
|- ( x = C -> ( ps <-> th ) )
reu2eqd.3 
|- ( ph -> E! x e. A ps )
reu2eqd.4 
|- ( ph -> B e. A )
reu2eqd.5 
|- ( ph -> C e. A )
reu2eqd.6 
|- ( ph -> ch )
reu2eqd.7 
|- ( ph -> th )
Assertion reu2eqd 
|- ( ph -> B = C )

Proof

Step Hyp Ref Expression
1 reu2eqd.1 
 |-  ( x = B -> ( ps <-> ch ) )
2 reu2eqd.2 
 |-  ( x = C -> ( ps <-> th ) )
3 reu2eqd.3 
 |-  ( ph -> E! x e. A ps )
4 reu2eqd.4 
 |-  ( ph -> B e. A )
5 reu2eqd.5 
 |-  ( ph -> C e. A )
6 reu2eqd.6 
 |-  ( ph -> ch )
7 reu2eqd.7 
 |-  ( ph -> th )
8 reu2 
 |-  ( E! x e. A ps <-> ( E. x e. A ps /\ A. x e. A A. y e. A ( ( ps /\ [ y / x ] ps ) -> x = y ) ) )
9 3 8 sylib 
 |-  ( ph -> ( E. x e. A ps /\ A. x e. A A. y e. A ( ( ps /\ [ y / x ] ps ) -> x = y ) ) )
10 9 simprd 
 |-  ( ph -> A. x e. A A. y e. A ( ( ps /\ [ y / x ] ps ) -> x = y ) )
11 nfv 
 |-  F/ x ch
12 nfs1v 
 |-  F/ x [ y / x ] ps
13 11 12 nfan 
 |-  F/ x ( ch /\ [ y / x ] ps )
14 nfv 
 |-  F/ x B = y
15 13 14 nfim 
 |-  F/ x ( ( ch /\ [ y / x ] ps ) -> B = y )
16 nfv 
 |-  F/ y ( ( ch /\ th ) -> B = C )
17 1 anbi1d 
 |-  ( x = B -> ( ( ps /\ [ y / x ] ps ) <-> ( ch /\ [ y / x ] ps ) ) )
18 eqeq1 
 |-  ( x = B -> ( x = y <-> B = y ) )
19 17 18 imbi12d 
 |-  ( x = B -> ( ( ( ps /\ [ y / x ] ps ) -> x = y ) <-> ( ( ch /\ [ y / x ] ps ) -> B = y ) ) )
20 nfv 
 |-  F/ x th
21 20 2 sbhypf 
 |-  ( y = C -> ( [ y / x ] ps <-> th ) )
22 21 anbi2d 
 |-  ( y = C -> ( ( ch /\ [ y / x ] ps ) <-> ( ch /\ th ) ) )
23 eqeq2 
 |-  ( y = C -> ( B = y <-> B = C ) )
24 22 23 imbi12d 
 |-  ( y = C -> ( ( ( ch /\ [ y / x ] ps ) -> B = y ) <-> ( ( ch /\ th ) -> B = C ) ) )
25 15 16 19 24 rspc2 
 |-  ( ( B e. A /\ C e. A ) -> ( A. x e. A A. y e. A ( ( ps /\ [ y / x ] ps ) -> x = y ) -> ( ( ch /\ th ) -> B = C ) ) )
26 4 5 25 syl2anc 
 |-  ( ph -> ( A. x e. A A. y e. A ( ( ps /\ [ y / x ] ps ) -> x = y ) -> ( ( ch /\ th ) -> B = C ) ) )
27 10 26 mpd 
 |-  ( ph -> ( ( ch /\ th ) -> B = C ) )
28 6 7 27 mp2and 
 |-  ( ph -> B = C )