This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )