moi

Description: Equality implied by "at most one". (Contributed by NM, 18-Feb-2006)

	Ref	Expression
Hypotheses	moi.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	moi.2	$⊢ x = B \to (φ \leftrightarrow χ)$
Assertion	moi	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ \land (ψ \land χ)) \to A = B$

Step	Hyp	Ref	Expression
1		moi.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		moi.2	$⊢ x = B \to (φ \leftrightarrow χ)$
3	1 2	mob	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ)$
4	3	biimprd	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ \land ψ) \to (χ \to A = B)$
5	4	3expia	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ) \to (ψ \to (χ \to A = B))$
6	5	impd	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ) \to ((ψ \land χ) \to A = B)$
7	6	3impia	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ \land (ψ \land χ)) \to A = B$

Metamath Proof Explorer