Theorem mob2

Description: Consequence of "at most one". (Contributed by NM, 2-Jan-2015)

	Ref	Expression
Hypothesis	moi2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	mob2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝑥 = 𝐴 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		moi2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		simp3	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → 𝜑 )
3	2 1	syl5ibcom	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝑥 = 𝐴 → 𝜓 ) )
4		nfv	⊢ Ⅎ 𝑥 𝜓
5	4 1	sbhypf	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
6	5	anbi2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
7		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
8	6 7	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝐴 ) ) )
9	8	spcgv	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝐴 ) ) )
10		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
11		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
12	10 11	mo4f	⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
13		sp	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
14	12 13	sylbi	⊢ ( ∃* 𝑥 𝜑 → ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
15	9 14	impel	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝐴 ) )
16	15	expd	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ) → ( 𝜑 → ( 𝜓 → 𝑥 = 𝐴 ) ) )
17	16	3impia	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝜓 → 𝑥 = 𝐴 ) )
18	3 17	impbid	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝑥 = 𝐴 ↔ 𝜓 ) )