Theorem funopabeq

Description: A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995)

	Ref	Expression
Assertion	funopabeq	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|y=A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funopab	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|y=A\right\}\leftrightarrow \forall x{\exists }^{*}yy=A$$
2		moeq	$$⊢{\exists }^{*}yy=A$$
3	1 2	mpgbir	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|y=A\right\}$$