Theorem opabex

Description: Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996)

	Ref	Expression
Hypotheses	opabex.1	$$⊢A\in \mathrm{V}$$
	opabex.2	$$⊢x\in A\to {\exists }^{*}y\phi$$
Assertion	opabex	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		opabex.1	$$⊢A\in \mathrm{V}$$
2		opabex.2	$$⊢x\in A\to {\exists }^{*}y\phi$$
3		funopab	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\leftrightarrow \forall x{\exists }^{*}y\left(x\in A\wedge \phi \right)$$
4		moanimv	$$⊢{\exists }^{*}y\left(x\in A\wedge \phi \right)\leftrightarrow \left(x\in A\to {\exists }^{*}y\phi \right)$$
5	2 4	mpbir	$$⊢{\exists }^{*}y\left(x\in A\wedge \phi \right)$$
6	3 5	mpgbir	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
7		dmopabss	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$
8	1 7	ssexi	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
9		funex	$$⊢\left(\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\wedge \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}\right)\to \left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
10	6 8 9	mp2an	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$