MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funfn Unicode version

Theorem funfn 5299
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn  |-  ( Fun 
A  <->  A  Fn  dom  A )

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2296 . . 3  |-  dom  A  =  dom  A
21biantru 491 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5274 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 243 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1632   dom cdm 4705   Fun wfun 5265    Fn wfn 5266
This theorem is referenced by:  funssxp  5418  funforn  5474  funbrfvb  5581  funopfvb  5582  ssimaex  5600  fvco  5611  fvco4i  5613  eqfunfv  5643  fvimacnvi  5655  unpreima  5667  respreima  5670  ffvresb  5706  funressn  5722  resfunexg  5753  funex  5759  funiunfv  5790  elunirnALT  5795  smores  6385  smores2  6387  rdgsucg  6452  rdglimg  6454  mptfi  7171  ordtypelem4  7252  ordtypelem6  7254  ordtypelem7  7255  ordtypelem9  7257  ordtypelem10  7258  harwdom  7320  ackbij2  7885  brdom3  8169  brdom5  8170  brdom4  8171  smobeth  8224  fpwwe2lem11  8278  hashkf  11355  hashfun  11405  fclim  12043  isstruct2  13173  xpsc0  13478  xpsc1  13479  invf  13686  coapm  13919  dfac14  17328  perfdvf  19269  c1lip2  19361  taylf  19756  hlimf  21833  adj1o  22490  abrexdomjm  23181  unipreima  23224  xppreima  23226  mptct  23360  mptctf  23363  orvcval2  23674  wfrlem4  24330  frrlem4  24355  elno3  24380  fullfunfnv  24556  fullfunfv  24557  abrexdom  26508  lindfrn  27394  psgnghm  27540  funcoressn  28095  funbrafvb  28124  funopafvb  28125  diaf11N  31861  dibf11N  31973
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289  df-fn 5274
  Copyright terms: Public domain W3C validator