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

Metamath Proof Explorer

Theorem moi2

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

		Ref	Expression
	Hypothesis	moi2.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	moi2	$⊢ ((A \in B \land \exists^{*} x φ) \land (φ \land ψ)) \to x = A$

Step	Hyp	Ref	Expression
1		moi2.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2	1	mob2	$⊢ (A \in B \land \exists^{*} x φ \land φ) \to (x = A \leftrightarrow ψ)$
3	2	3expa	$⊢ ((A \in B \land \exists^{*} x φ) \land φ) \to (x = A \leftrightarrow ψ)$
4	3	biimprd	$⊢ ((A \in B \land \exists^{*} x φ) \land φ) \to (ψ \to x = A)$
5	4	impr	$⊢ ((A \in B \land \exists^{*} x φ) \land (φ \land ψ)) \to x = A$