Theorem fnopabg

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004) (Proof shortened by Mario Carneiro, 4-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		fnopabg.1	|- F = { <. x , y >. | ( x e. A /\ ph ) }
2		moanimv	|- ( E* y ( x e. A /\ ph ) <-> ( x e. A -> E* y ph ) )
3	2	albii	|- ( A. x E* y ( x e. A /\ ph ) <-> A. x ( x e. A -> E* y ph ) )
4		funopab	|- ( Fun { <. x , y >. | ( x e. A /\ ph ) } <-> A. x E* y ( x e. A /\ ph ) )
5		df-ral	|- ( A. x e. A E* y ph <-> A. x ( x e. A -> E* y ph ) )
6	3 4 5	3bitr4ri	|- ( A. x e. A E* y ph <-> Fun { <. x , y >. | ( x e. A /\ ph ) } )
7		dmopab3	|- ( A. x e. A E. y ph <-> dom { <. x , y >. | ( x e. A /\ ph ) } = A )
8	6 7	anbi12i	|- ( ( A. x e. A E* y ph /\ A. x e. A E. y ph ) <-> ( Fun { <. x , y >. | ( x e. A /\ ph ) } /\ dom { <. x , y >. | ( x e. A /\ ph ) } = A ) )
9		r19.26	|- ( A. x e. A ( E* y ph /\ E. y ph ) <-> ( A. x e. A E* y ph /\ A. x e. A E. y ph ) )
10		df-fn	|- ( { <. x , y >. | ( x e. A /\ ph ) } Fn A <-> ( Fun { <. x , y >. | ( x e. A /\ ph ) } /\ dom { <. x , y >. | ( x e. A /\ ph ) } = A ) )
11	8 9 10	3bitr4i	|- ( A. x e. A ( E* y ph /\ E. y ph ) <-> { <. x , y >. | ( x e. A /\ ph ) } Fn A )
12		df-eu	|- ( E! y ph <-> ( E. y ph /\ E* y ph ) )
13	12	biancomi	|- ( E! y ph <-> ( E* y ph /\ E. y ph ) )
14	13	ralbii	|- ( A. x e. A E! y ph <-> A. x e. A ( E* y ph /\ E. y ph ) )
15	1	fneq1i	|- ( F Fn A <-> { <. x , y >. | ( x e. A /\ ph ) } Fn A )
16	11 14 15	3bitr4i	|- ( A. x e. A E! y ph <-> F Fn A )