Metamath Proof Explorer

Theorem reuxfrd

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . (Contributed by NM, 16-Jan-2012) Separate variables B and C. (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses reuxfrd.1 
|- ( ( ph /\ y e. C ) -> A e. B )
reuxfrd.2 
|- ( ( ph /\ x e. B ) -> E* y e. C x = A )
Assertion reuxfrd 
|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C ps ) )

Proof

Step Hyp Ref Expression
1 reuxfrd.1 
 |-  ( ( ph /\ y e. C ) -> A e. B )
2 reuxfrd.2 
 |-  ( ( ph /\ x e. B ) -> E* y e. C x = A )
3 rmoan 
 |-  ( E* y e. C x = A -> E* y e. C ( ps /\ x = A ) )
4 2 3 syl 
 |-  ( ( ph /\ x e. B ) -> E* y e. C ( ps /\ x = A ) )
5 ancom 
 |-  ( ( ps /\ x = A ) <-> ( x = A /\ ps ) )
6 5 rmobii 
 |-  ( E* y e. C ( ps /\ x = A ) <-> E* y e. C ( x = A /\ ps ) )
7 4 6 sylib 
 |-  ( ( ph /\ x e. B ) -> E* y e. C ( x = A /\ ps ) )
8 7 ralrimiva 
 |-  ( ph -> A. x e. B E* y e. C ( x = A /\ ps ) )
9 2reuswap 
 |-  ( A. x e. B E* y e. C ( x = A /\ ps ) -> ( E! x e. B E. y e. C ( x = A /\ ps ) -> E! y e. C E. x e. B ( x = A /\ ps ) ) )
10 8 9 syl 
 |-  ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) -> E! y e. C E. x e. B ( x = A /\ ps ) ) )
11 2reuswap2 
 |-  ( A. y e. C E* x ( x e. B /\ ( x = A /\ ps ) ) -> ( E! y e. C E. x e. B ( x = A /\ ps ) -> E! x e. B E. y e. C ( x = A /\ ps ) ) )
12 moeq 
 |-  E* x x = A
13 12 moani 
 |-  E* x ( ( x e. B /\ ps ) /\ x = A )
14 ancom 
 |-  ( ( ( x e. B /\ ps ) /\ x = A ) <-> ( x = A /\ ( x e. B /\ ps ) ) )
15 an12 
 |-  ( ( x = A /\ ( x e. B /\ ps ) ) <-> ( x e. B /\ ( x = A /\ ps ) ) )
16 14 15 bitri 
 |-  ( ( ( x e. B /\ ps ) /\ x = A ) <-> ( x e. B /\ ( x = A /\ ps ) ) )
17 16 mobii 
 |-  ( E* x ( ( x e. B /\ ps ) /\ x = A ) <-> E* x ( x e. B /\ ( x = A /\ ps ) ) )
18 13 17 mpbi 
 |-  E* x ( x e. B /\ ( x = A /\ ps ) )
19 18 a1i 
 |-  ( y e. C -> E* x ( x e. B /\ ( x = A /\ ps ) ) )
20 11 19 mprg 
 |-  ( E! y e. C E. x e. B ( x = A /\ ps ) -> E! x e. B E. y e. C ( x = A /\ ps ) )
21 10 20 impbid1 
 |-  ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C E. x e. B ( x = A /\ ps ) ) )
22 biidd 
 |-  ( x = A -> ( ps <-> ps ) )
23 22 ceqsrexv 
 |-  ( A e. B -> ( E. x e. B ( x = A /\ ps ) <-> ps ) )
24 1 23 syl 
 |-  ( ( ph /\ y e. C ) -> ( E. x e. B ( x = A /\ ps ) <-> ps ) )
25 24 reubidva 
 |-  ( ph -> ( E! y e. C E. x e. B ( x = A /\ ps ) <-> E! y e. C ps ) )
26 21 25 bitrd 
 |-  ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C ps ) )