Theorem fnopab

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996)

	Ref	Expression
Hypotheses	fnopab.1	$$⊢x\in A\to \exists !y\phi$$
	fnopab.2	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
Assertion	fnopab	$$⊢FFnA$$

Proof

Step	Hyp	Ref	Expression
1		fnopab.1	$$⊢x\in A\to \exists !y\phi$$
2		fnopab.2	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
3	1	rgen	$$⊢\forall x\in A\exists !y\phi$$
4	2	fnopabg	$$⊢\forall x\in A\exists !y\phi \leftrightarrow FFnA$$
5	3 4	mpbi	$$⊢FFnA$$