mob

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	mob	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		moi.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		moi.2	$⊢ x = B \to (φ \leftrightarrow χ)$
3		elex	$⊢ B \in D \to B \in V$
4		nfv	$⊢ Ⅎ x B \in V$
5		nfmo1	$⊢ Ⅎ x \exists^{*} x φ$
6		nfv	$⊢ Ⅎ x ψ$
7	4 5 6	nf3an	$⊢ Ⅎ x (B \in V \land \exists^{*} x φ \land ψ)$
8		nfv	$⊢ Ⅎ x (A = B \leftrightarrow χ)$
9	7 8	nfim	$⊢ Ⅎ x ((B \in V \land \exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ))$
10	1	3anbi3d	$⊢ x = A \to ((B \in V \land \exists^{} x φ \land φ) \leftrightarrow (B \in V \land \exists^{} x φ \land ψ))$
11		eqeq1	$⊢ x = A \to (x = B \leftrightarrow A = B)$
12	11	bibi1d	$⊢ x = A \to ((x = B \leftrightarrow χ) \leftrightarrow (A = B \leftrightarrow χ))$
13	10 12	imbi12d	$⊢ x = A \to (((B \in V \land \exists^{} x φ \land φ) \to (x = B \leftrightarrow χ)) \leftrightarrow ((B \in V \land \exists^{} x φ \land ψ) \to (A = B \leftrightarrow χ)))$
14	2	mob2	$⊢ (B \in V \land \exists^{*} x φ \land φ) \to (x = B \leftrightarrow χ)$
15	9 13 14	vtoclg1f	$⊢ A \in C \to ((B \in V \land \exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ))$
16	15	com12	$⊢ (B \in V \land \exists^{*} x φ \land ψ) \to (A \in C \to (A = B \leftrightarrow χ))$
17	16	3expib	$⊢ B \in V \to ((\exists^{*} x φ \land ψ) \to (A \in C \to (A = B \leftrightarrow χ)))$
18	3 17	syl	$⊢ B \in D \to ((\exists^{*} x φ \land ψ) \to (A \in C \to (A = B \leftrightarrow χ)))$
19	18	com3r	$⊢ A \in C \to (B \in D \to ((\exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ)))$
20	19	imp	$⊢ (A \in C \land B \in D) \to ((\exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ))$
21	20	3impib	$⊢ ((A \in C \land B \in D) \land \exists^{*} x φ \land ψ) \to (A = B \leftrightarrow χ)$

Metamath Proof Explorer

Theorem mob

Proof