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

Theorem funfn 5482
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 2436 . . 3  |-  dom  A  =  dom  A
21biantru 492 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5457 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 244 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1652   dom cdm 4878   Fun wfun 5448    Fn wfn 5449
This theorem is referenced by:  funssxp  5604  funforn  5660  funbrfvb  5769  funopfvb  5770  ssimaex  5788  fvco  5799  fvco4i  5801  eqfunfv  5832  fvimacnvi  5844  unpreima  5856  respreima  5859  elrnrexdm  5874  elrnrexdmb  5875  ffvresb  5900  funressn  5919  resfunexg  5957  funex  5963  funiunfv  5995  elunirnALT  6000  smores  6614  smores2  6616  rdgsucg  6681  rdglimg  6683  mptfi  7406  ordtypelem4  7490  ordtypelem6  7492  ordtypelem7  7493  ordtypelem9  7495  ordtypelem10  7496  harwdom  7558  ackbij2  8123  brdom3  8406  brdom5  8407  brdom4  8408  smobeth  8461  fpwwe2lem11  8515  hashkf  11620  hashfun  11700  fclim  12347  isstruct2  13478  xpsc0  13785  xpsc1  13786  invf  13993  coapm  14226  dfac14  17650  perfdvf  19790  c1lip2  19882  taylf  20277  usgra2edg  21402  usgrarnedg  21404  usgrafilem2  21426  cusgrares  21481  vdusgraval  21678  vdgrnn0pnf  21680  hlimf  22740  adj1o  23397  abrexdomjm  23988  unipreima  24056  xppreima  24059  mptct  24109  mptctf  24112  sitgf  24660  orvcval2  24716  wfrlem4  25541  frrlem4  25585  elno3  25610  fullfunfnv  25791  fullfunfv  25792  abrexdom  26432  lindfrn  27268  psgnghm  27414  funcoressn  27967  funbrafvb  27996  funopafvb  27997  resfnfinfin  28086  hashimarn  28163  vdn0frgrav2  28414  vdgn0frgrav2  28415  vdgfrgragt2  28418  diaf11N  31847  dibf11N  31959
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-cleq 2429  df-fn 5457
  Copyright terms: Public domain W3C validator