Theorem eqeu

Description: A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009)

	Ref	Expression
Hypothesis	eqeu.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	eqeu	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) → ∃! 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		eqeu.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2	1	spcegv	⊢ ( 𝐴 ∈ 𝐵 → ( 𝜓 → ∃ 𝑥 𝜑 ) )
3	2	imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 𝜑 )
4	3	3adant3	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) → ∃ 𝑥 𝜑 )
5		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
6	5	imbi2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 → 𝑥 = 𝐴 ) ) )
7	6	albidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) )
8	7	spcegv	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
9	8	imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
10	9	3adant2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
11		eu3v	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
12	4 10 11	sylanbrc	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) → ∃! 𝑥 𝜑 )