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

Theorem funfn 5615
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 2467 . . 3  |-  dom  A  =  dom  A
21biantru 505 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5589 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 252 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1379   dom cdm 4999   Fun wfun 5580    Fn wfn 5581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5589
This theorem is referenced by:  funssxp  5742  funforn  5800  funbrfvb  5908  funopfvb  5909  ssimaex  5930  fvco  5941  fvco4i  5943  eqfunfv  5978  fvimacnvi  5993  unpreima  6005  respreima  6008  elrnrexdm  6023  elrnrexdmb  6024  ffvresb  6050  funressn  6072  funresdfunsn  6101  resfunexg  6124  funex  6126  funiunfv  6146  elunirn  6149  suppval1  6904  funsssuppss  6923  smores  7020  smores2  7022  tfrlem1  7042  rdgsucg  7086  rdglimg  7088  mptfi  7815  resfifsupp  7853  ordtypelem4  7942  ordtypelem6  7944  ordtypelem7  7945  ordtypelem9  7947  ordtypelem10  7948  harwdom  8012  ackbij2  8619  brdom3  8902  brdom5  8903  brdom4  8904  smobeth  8957  fpwwe2lem11  9014  hashkf  12371  hashfun  12457  hashimarn  12458  fclim  13335  isstruct2  14495  xpsc0  14811  xpsc1  14812  invf  15019  coapm  15252  psgnghm  18383  lindfrn  18623  ofco2  18720  dfac14  19854  perfdvf  22042  c1lip2  22134  taylf  22490  usgra2edg  24058  usgrarnedg  24060  usgrafilem2  24088  cusgrares  24148  vdusgraval  24583  vdgrnn0pnf  24585  vdn0frgrav2  24700  vdgn0frgrav2  24701  vdgfrgragt2  24704  hlimf  25831  adj1o  26489  abrexdomjm  27079  iunpreima  27105  unipreima  27156  xppreima  27159  mptct  27213  mptctf  27216  sitgf  27929  orvcval2  28037  wfrlem4  28923  frrlem4  28967  elno3  28992  fullfunfnv  29173  fullfunfv  29174  abrexdom  29824  funcoressn  31679  funbrafvb  31708  funopafvb  31709  resfnfinfin  31779  fundmfibi  31780  residfi  31783  uhgraopsiz  31861  diaf11N  35846  dibf11N  35958
  Copyright terms: Public domain W3C validator