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 φ B
renegeulemv.1 φ y B + y = A
Assertion renegeulemv φ ∃! x B + x = A

Proof

Step Hyp Ref Expression
1 renegeulemv.b φ B
2 renegeulemv.1 φ y B + y = A
3 simprl φ y B + y = A y
4 simplrr φ y B + y = A x B + y = A
5 4 eqcomd φ y B + y = A x A = B + y
6 5 eqeq2d φ y B + y = A x B + x = A B + x = B + y
7 simpr φ y B + y = A x x
8 simplrl φ y B + y = A x y
9 1 ad2antrr φ y B + y = A x B
10 readdcan x y B B + x = B + y x = y
11 7 8 9 10 syl3anc φ y B + y = A x B + x = B + y x = y
12 6 11 bitrd φ y B + y = A x B + x = A x = y
13 12 ralrimiva φ y B + y = A x B + x = A x = y
14 reu6i y x B + x = A x = y ∃! x B + x = A
15 3 13 14 syl2anc φ y B + y = A ∃! x B + x = A
16 2 15 rexlimddv φ ∃! x B + x = A