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

Metamath Proof Explorer

Theorem mo2icl

Description: Theorem for inferring "at most one". (Contributed by NM, 17-Oct-1996)

Ref Expression
Assertion mo2icl ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
2 1 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 → 𝑥 = 𝐴 ) ) )
3 2 albidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) )
4 3 imbi1d ⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 ) ) )
5 equequ2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
6 5 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 → 𝑥 = 𝑧 ) ) )
7 6 albidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
8 7 19.8aw ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
9 df-mo ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
10 8 9 sylibr ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 )
11 4 10 vtoclg ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 ) )
12 eqvisset ⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )
13 12 imim2i ⊢ ( ( 𝜑 → 𝑥 = 𝐴 ) → ( 𝜑 → 𝐴 ∈ V ) )
14 13 con3rr3 ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝜑 → 𝑥 = 𝐴 ) → ¬ 𝜑 ) )
15 14 alimdv ⊢ ( ¬ 𝐴 ∈ V → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∀ 𝑥 ¬ 𝜑 ) )
16 alnex ⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
17 nexmo ⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 )
18 16 17 sylbi ⊢ ( ∀ 𝑥 ¬ 𝜑 → ∃* 𝑥 𝜑 )
19 15 18 syl6 ⊢ ( ¬ 𝐴 ∈ V → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 ) )
20 11 19 pm2.61i ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 )