morex

Description: Derive membership from uniqueness. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Step	Hyp	Ref	Expression
1		morex.1	$⊢ B \in V$
2		morex.2	$⊢ x = B \to (φ \leftrightarrow ψ)$
3		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
4		exancom	$⊢ \exists x (x \in A \land φ) \leftrightarrow \exists x (φ \land x \in A)$
5	3 4	bitri	$⊢ \exists x \in A φ \leftrightarrow \exists x (φ \land x \in A)$
6		nfmo1	$⊢ Ⅎ x \exists^{*} x φ$
7		nfe1	$⊢ Ⅎ x \exists x (φ \land x \in A)$
8	6 7	nfan	$⊢ Ⅎ x (\exists^{*} x φ \land \exists x (φ \land x \in A))$
9		mopick	$⊢ (\exists^{*} x φ \land \exists x (φ \land x \in A)) \to (φ \to x \in A)$
10	8 9	alrimi	$⊢ (\exists^{*} x φ \land \exists x (φ \land x \in A)) \to \forall x (φ \to x \in A)$
11		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
12	2 11	imbi12d	$⊢ x = B \to ((φ \to x \in A) \leftrightarrow (ψ \to B \in A))$
13	1 12	spcv	$⊢ \forall x (φ \to x \in A) \to (ψ \to B \in A)$
14	10 13	syl	$⊢ (\exists^{*} x φ \land \exists x (φ \land x \in A)) \to (ψ \to B \in A)$
15	5 14	sylan2b	$⊢ (\exists^{*} x φ \land \exists x \in A φ) \to (ψ \to B \in A)$
16	15	ancoms	$⊢ (\exists x \in A φ \land \exists^{*} x φ) \to (ψ \to B \in A)$

Metamath Proof Explorer