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		19.8a	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
6		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
7	5 6	sylibr	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 )
8	4 7	vtoclg	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 ) )
9		eqvisset	⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )
10	9	imim2i	⊢ ( ( 𝜑 → 𝑥 = 𝐴 ) → ( 𝜑 → 𝐴 ∈ V ) )
11	10	con3rr3	⊢ ( ¬ 𝐴 ∈ V → ( ( 𝜑 → 𝑥 = 𝐴 ) → ¬ 𝜑 ) )
12	11	alimdv	⊢ ( ¬ 𝐴 ∈ V → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∀ 𝑥 ¬ 𝜑 ) )
13		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
14		nexmo	⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 )
15	13 14	sylbi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∃* 𝑥 𝜑 )
16	12 15	syl6	⊢ ( ¬ 𝐴 ∈ V → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 ) )
17	8 16	pm2.61i	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 )