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		dfmo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
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	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ∃* 𝑥 𝜑 )