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

Theorem funfn 5441
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 2404 . . 3  |-  dom  A  =  dom  A
21biantru 492 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5416 . 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 1649   dom cdm 4837   Fun wfun 5407    Fn wfn 5408
This theorem is referenced by:  funssxp  5563  funforn  5619  funbrfvb  5728  funopfvb  5729  ssimaex  5747  fvco  5758  fvco4i  5760  eqfunfv  5791  fvimacnvi  5803  unpreima  5815  respreima  5818  elrnrexdm  5833  elrnrexdmb  5834  ffvresb  5859  funressn  5878  resfunexg  5916  funex  5922  funiunfv  5954  elunirnALT  5959  smores  6573  smores2  6575  rdgsucg  6640  rdglimg  6642  mptfi  7364  ordtypelem4  7446  ordtypelem6  7448  ordtypelem7  7449  ordtypelem9  7451  ordtypelem10  7452  harwdom  7514  ackbij2  8079  brdom3  8362  brdom5  8363  brdom4  8364  smobeth  8417  fpwwe2lem11  8471  hashkf  11575  hashfun  11655  fclim  12302  isstruct2  13433  xpsc0  13740  xpsc1  13741  invf  13948  coapm  14181  dfac14  17603  perfdvf  19743  c1lip2  19835  taylf  20230  usgra2edg  21355  usgrarnedg  21357  usgrafilem2  21379  cusgrares  21434  vdusgraval  21631  vdgrnn0pnf  21633  hlimf  22693  adj1o  23350  abrexdomjm  23941  unipreima  24009  xppreima  24012  mptct  24062  mptctf  24065  sitgf  24613  orvcval2  24669  wfrlem4  25473  frrlem4  25498  elno3  25523  fullfunfnv  25699  fullfunfv  25700  abrexdom  26322  lindfrn  27159  psgnghm  27305  funcoressn  27858  funbrafvb  27887  funopafvb  27888  resfnfinfin  27966  hashimarn  27994  vdn0frgrav2  28128  vdgn0frgrav2  28129  vdgfrgragt2  28132  diaf11N  31532  dibf11N  31644
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-cleq 2397  df-fn 5416
  Copyright terms: Public domain W3C validator