Metamath Proof Explorer


Theorem renegeulemv

Description: Lemma for renegeu and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023)

Ref Expression
Hypotheses renegeulemv.b
|- ( ph -> B e. RR )
renegeulemv.1
|- ( ph -> E. y e. RR ( B + y ) = A )
Assertion renegeulemv
|- ( ph -> E! x e. RR ( B + x ) = A )

Proof

Step Hyp Ref Expression
1 renegeulemv.b
 |-  ( ph -> B e. RR )
2 renegeulemv.1
 |-  ( ph -> E. y e. RR ( B + y ) = A )
3 simprl
 |-  ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) -> y e. RR )
4 simplrr
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> ( B + y ) = A )
5 4 eqcomd
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> A = ( B + y ) )
6 5 eqeq2d
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> ( ( B + x ) = A <-> ( B + x ) = ( B + y ) ) )
7 simpr
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> x e. RR )
8 simplrl
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> y e. RR )
9 1 ad2antrr
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> B e. RR )
10 readdcan
 |-  ( ( x e. RR /\ y e. RR /\ B e. RR ) -> ( ( B + x ) = ( B + y ) <-> x = y ) )
11 7 8 9 10 syl3anc
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> ( ( B + x ) = ( B + y ) <-> x = y ) )
12 6 11 bitrd
 |-  ( ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) /\ x e. RR ) -> ( ( B + x ) = A <-> x = y ) )
13 12 ralrimiva
 |-  ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) -> A. x e. RR ( ( B + x ) = A <-> x = y ) )
14 reu6i
 |-  ( ( y e. RR /\ A. x e. RR ( ( B + x ) = A <-> x = y ) ) -> E! x e. RR ( B + x ) = A )
15 3 13 14 syl2anc
 |-  ( ( ph /\ ( y e. RR /\ ( B + y ) = A ) ) -> E! x e. RR ( B + x ) = A )
16 2 15 rexlimddv
 |-  ( ph -> E! x e. RR ( B + x ) = A )