This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) ) )
6 reu6i ⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
7 6 ex ⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝐵 ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
8 5 7 sylbird ⊢ ( 𝐵 ∈ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
9 8 3impib ⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
10 9 3com23 ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝐵 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )