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

Metamath Proof Explorer

Theorem rmorabex

Description: Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017)

Ref Expression
Assertion rmorabex ⊢ ∃* x ∈ A φ → x ∈ A | φ ∈ V

Proof

Step Hyp Ref Expression
1 moabex ⊢ ∃* x x ∈ A ∧ φ → x | x ∈ A ∧ φ ∈ V
2 df-rmo ⊢ ∃* x ∈ A φ ↔ ∃* x x ∈ A ∧ φ
3 df-rab ⊢ x ∈ A | φ = x | x ∈ A ∧ φ
4 3 eleq1i ⊢ x ∈ A | φ ∈ V ↔ x | x ∈ A ∧ φ ∈ V
5 1 2 4 3imtr4i ⊢ ∃* x ∈ A φ → x ∈ A | φ ∈ V