Theorem rmorabex

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

	Ref	Expression
Assertion	rmorabex	$$⊢{\exists }^{*}x\in A\phi \to \left\{x\in A|\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		moabex	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)\to \left\{x|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
2		df-rmo	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \phi \right)$$
3		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
4	3	eleq1i	$$⊢\left\{x\in A|\phi \right\}\in \mathrm{V}\leftrightarrow \left\{x|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
5	1 2 4	3imtr4i	$$⊢{\exists }^{*}x\in A\phi \to \left\{x\in A|\phi \right\}\in \mathrm{V}$$