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

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 )