ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fnopab Unicode version

Theorem fnopab 5329
Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.)
Hypotheses
Ref Expression
fnopab.1  |-  ( x  e.  A  ->  E! y ph )
fnopab.2  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  ph ) }
Assertion
Ref Expression
fnopab  |-  F  Fn  A
Distinct variable group:    x, y, A
Allowed substitution hints:    ph( x, y)    F( x, y)

Proof of Theorem fnopab
StepHypRef Expression
1 fnopab.1 . . 3  |-  ( x  e.  A  ->  E! y ph )
21rgen 2526 . 2  |-  A. x  e.  A  E! y ph
3 fnopab.2 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  ph ) }
43fnopabg 5328 . 2  |-  ( A. x  e.  A  E! y ph  <->  F  Fn  A
)
52, 4mpbi 146 1  |-  F  Fn  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1351   E!weu 2022    e. wcel 2144   A.wral 2451   {copab 4055    Fn wfn 5200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 707  ax-5 1443  ax-7 1444  ax-gen 1445  ax-ie1 1489  ax-ie2 1490  ax-8 1500  ax-10 1501  ax-11 1502  ax-i12 1503  ax-bndl 1505  ax-4 1506  ax-17 1522  ax-i9 1526  ax-ial 1530  ax-i5r 1531  ax-14 2147  ax-ext 2155  ax-sep 4113  ax-pow 4166  ax-pr 4200
This theorem depends on definitions:  df-bi 117  df-3an 978  df-tru 1354  df-nf 1457  df-sb 1759  df-eu 2025  df-mo 2026  df-clab 2160  df-cleq 2166  df-clel 2169  df-nfc 2304  df-ral 2456  df-rex 2457  df-v 2735  df-un 3128  df-in 3130  df-ss 3137  df-pw 3571  df-sn 3592  df-pr 3593  df-op 3595  df-br 3996  df-opab 4057  df-id 4284  df-xp 4623  df-rel 4624  df-cnv 4625  df-co 4626  df-dm 4627  df-fun 5207  df-fn 5208
This theorem is referenced by:  fvopab3g  5578
  Copyright terms: Public domain W3C validator