Theorem morex

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

	Ref	Expression
Hypotheses	morex.1	⊢ 𝐵 ∈ V
	morex.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion	morex	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 𝜑 ) → ( 𝜓 → 𝐵 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		morex.1	⊢ 𝐵 ∈ V
2		morex.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
3		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
4		exancom	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
5	3 4	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
6		nfmo1	⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
7		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
8	6 7	nfan	⊢ Ⅎ 𝑥 ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
9		mopick	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝜑 → 𝑥 ∈ 𝐴 ) )
10	8 9	alrimi	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ) → ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝐴 ) )
11		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
12	2 11	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝜑 → 𝑥 ∈ 𝐴 ) ↔ ( 𝜓 → 𝐵 ∈ 𝐴 ) ) )
13	1 12	spcv	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝐵 ∈ 𝐴 ) )
14	10 13	syl	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝜓 → 𝐵 ∈ 𝐴 ) )
15	5 14	sylan2b	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 → 𝐵 ∈ 𝐴 ) )
16	15	ancoms	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 𝜑 ) → ( 𝜓 → 𝐵 ∈ 𝐴 ) )