Theorem fnopab

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

	Ref	Expression
Hypotheses	fnopab.1	|- ( x e. A -> E! y ph )
	fnopab.2	|- F = { <. x , y >. | ( x e. A /\ ph ) }
Assertion	fnopab	|- F Fn A

Proof

Step	Hyp	Ref	Expression
1		fnopab.1	|- ( x e. A -> E! y ph )
2		fnopab.2	|- F = { <. x , y >. | ( x e. A /\ ph ) }
3	1	rgen	|- A. x e. A E! y ph
4	2	fnopabg	|- ( A. x e. A E! y ph <-> F Fn A )
5	3 4	mpbi	|- F Fn A