Theorem funopab4

Description: A class of ordered pairs of values in the form used by df-mpt is a function. (Contributed by NM, 17-Feb-2013)

	Ref	Expression
Assertion	funopab4	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(\phi \wedge y=A\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\phi \wedge y=A\right)\to y=A$$
2	1	ssopab2i	$$⊢\left\{⟨x,y⟩|\left(\phi \wedge y=A\right)\right\}\subseteq \left\{⟨x,y⟩|y=A\right\}$$
3		funopabeq	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|y=A\right\}$$
4		funss	$$⊢\left\{⟨x,y⟩|\left(\phi \wedge y=A\right)\right\}\subseteq \left\{⟨x,y⟩|y=A\right\}\to \left(\mathrm{Fun}\left\{⟨x,y⟩|y=A\right\}\to \mathrm{Fun}\left\{⟨x,y⟩|\left(\phi \wedge y=A\right)\right\}\right)$$
5	2 3 4	mp2	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(\phi \wedge y=A\right)\right\}$$