Theorem moi2

Description: Consequence of "at most one." (Contributed by NM, 29-Jun-2008)

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

Proof

Step	Hyp	Ref	Expression
1		moi2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2	1	mob2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ∧ 𝜑 ) → ( 𝑥 = 𝐴 ↔ 𝜓 ) )
3	2	3expa	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ) ∧ 𝜑 ) → ( 𝑥 = 𝐴 ↔ 𝜓 ) )
4	3	biimprd	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ) ∧ 𝜑 ) → ( 𝜓 → 𝑥 = 𝐴 ) )
5	4	impr	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∃* 𝑥 𝜑 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝑥 = 𝐴 )