Theorem reuhyp

Description: A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 . (Contributed by NM, 15-Nov-2004)

	Ref	Expression
Hypotheses	reuhyp.1	⊢ ( 𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶 )
	reuhyp.2	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐵 ) )
Assertion	reuhyp	⊢ ( 𝑥 ∈ 𝐶 → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		reuhyp.1	⊢ ( 𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶 )
2		reuhyp.2	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐵 ) )
3		tru	⊢ ⊤
4	1	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
5	2	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐵 ) )
6	4 5	reuhypd	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐶 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
7	3 6	mpan	⊢ ( 𝑥 ∈ 𝐶 → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )