mob2

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

Step	Hyp	Ref	Expression
1		moi2.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		simp3	$⊢ (A \in B \land \exists^{*} x φ \land φ) \to φ$
3	2 1	syl5ibcom	$⊢ (A \in B \land \exists^{*} x φ \land φ) \to (x = A \to ψ)$
4		nfv	$⊢ Ⅎ x ψ$
5	4 1	sbhypf	$⊢ y = A \to ([y/ x] φ \leftrightarrow ψ)$
6	5	anbi2d	$⊢ y = A \to ((φ \land [y/ x] φ) \leftrightarrow (φ \land ψ))$
7		eqeq2	$⊢ y = A \to (x = y \leftrightarrow x = A)$
8	6 7	imbi12d	$⊢ y = A \to (((φ \land [y/ x] φ) \to x = y) \leftrightarrow ((φ \land ψ) \to x = A))$
9	8	spcgv	$⊢ A \in B \to (\forall y ((φ \land [y/ x] φ) \to x = y) \to ((φ \land ψ) \to x = A))$
10		nfs1v	$⊢ Ⅎ x [y/ x] φ$
11		sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$
12	10 11	mo4f	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land [y/ x] φ) \to x = y)$
13		sp	$⊢ \forall x \forall y ((φ \land [y/ x] φ) \to x = y) \to \forall y ((φ \land [y/ x] φ) \to x = y)$
14	12 13	sylbi	$⊢ \exists^{*} x φ \to \forall y ((φ \land [y/ x] φ) \to x = y)$
15	9 14	impel	$⊢ (A \in B \land \exists^{*} x φ) \to ((φ \land ψ) \to x = A)$
16	15	expd	$⊢ (A \in B \land \exists^{*} x φ) \to (φ \to (ψ \to x = A))$
17	16	3impia	$⊢ (A \in B \land \exists^{*} x φ \land φ) \to (ψ \to x = A)$
18	3 17	impbid	$⊢ (A \in B \land \exists^{*} x φ \land φ) \to (x = A \leftrightarrow ψ)$

Metamath Proof Explorer