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	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	renegeulemv.1	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝐵 + 𝑦 ) = 𝐴 )
Assertion	renegeulemv	⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		renegeulemv.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2		renegeulemv.1	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝐵 + 𝑦 ) = 𝐴 )
3		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) → 𝑦 ∈ ℝ )
4		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐵 + 𝑦 ) = 𝐴 )
5	4	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → 𝐴 = ( 𝐵 + 𝑦 ) )
6	5	eqeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 + 𝑥 ) = 𝐴 ↔ ( 𝐵 + 𝑥 ) = ( 𝐵 + 𝑦 ) ) )
7		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
8		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → 𝑦 ∈ ℝ )
9	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
10		readdcan	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 + 𝑥 ) = ( 𝐵 + 𝑦 ) ↔ 𝑥 = 𝑦 ) )
11	7 8 9 10	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 + 𝑥 ) = ( 𝐵 + 𝑦 ) ↔ 𝑥 = 𝑦 ) )
12	6 11	bitrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 + 𝑥 ) = 𝐴 ↔ 𝑥 = 𝑦 ) )
13	12	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) → ∀ 𝑥 ∈ ℝ ( ( 𝐵 + 𝑥 ) = 𝐴 ↔ 𝑥 = 𝑦 ) )
14		reu6i	⊢ ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ( ( 𝐵 + 𝑥 ) = 𝐴 ↔ 𝑥 = 𝑦 ) ) → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
15	3 13 14	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 + 𝑦 ) = 𝐴 ) ) → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
16	2 15	rexlimddv	⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )