This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 𝜑 ) → ( 𝜓 → 𝐵 ∈ 𝐴 ) )