Theorem eqreu

Description: A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eqreu.1	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2		ralbiim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 → 𝜑 ) ) )
3	1	ceqsralv	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 → 𝜑 ) ↔ 𝜓 ) )
4	3	anbi2d	⊢ ( 𝐵 ∈ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝐵 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) ) )
5	2 4	syl5bb	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) ) )
6		reu6i	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
7	6	ex	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
8	5 7	sylbird	⊢ ( 𝐵 ∈ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
9	8	3impib	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
10	9	3com23	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )