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

Theorem funfn 5599
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 2454 . . 3  |-  dom  A  =  dom  A
21biantru 503 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5573 . 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 367    = wceq 1398   dom cdm 4988   Fun wfun 5564    Fn wfn 5565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2446  df-fn 5573
This theorem is referenced by:  funssxp  5726  funforn  5784  funbrfvb  5890  funopfvb  5891  ssimaex  5913  fvco  5924  fvco4i  5926  eqfunfv  5962  fvimacnvi  5977  unpreima  5989  respreima  5992  elrnrexdm  6011  elrnrexdmb  6012  ffvresb  6038  funressn  6060  funresdfunsn  6089  resfunexg  6112  funex  6115  funiunfv  6135  elunirn  6138  suppval1  6897  funsssuppss  6918  smores  7015  smores2  7017  tfrlem1  7037  rdgsucg  7081  rdglimg  7083  mptfi  7811  resfifsupp  7849  ordtypelem4  7938  ordtypelem6  7940  ordtypelem7  7941  ordtypelem9  7943  ordtypelem10  7944  harwdom  8008  ackbij2  8614  brdom3  8897  brdom5  8898  brdom4  8899  smobeth  8952  fpwwe2lem11  9007  hashkf  12392  hashfun  12482  hashimarn  12483  fclim  13461  isstruct2  14728  xpsc0  15052  xpsc1  15053  invf  15259  coapm  15552  psgnghm  18792  lindfrn  19026  ofco2  19123  dfac14  20288  perfdvf  22476  c1lip2  22568  taylf  22925  usgra2edg  24587  usgrarnedg  24589  usgrafilem2  24617  cusgrares  24677  vdusgraval  25112  vdgrnn0pnf  25114  vdn0frgrav2  25228  vdgn0frgrav2  25229  vdgfrgragt2  25232  hlimf  26356  adj1o  27014  abrexdomjm  27607  iunpreima  27645  fresf1o  27695  unipreima  27708  xppreima  27711  mptct  27774  mptctf  27777  sitgf  28556  orvcval2  28664  wfrlem4  29589  frrlem4  29633  elno3  29658  fullfunfnv  29827  fullfunfv  29828  abrexdom  30464  funcoressn  32454  funbrafvb  32483  funopafvb  32484  resfnfinfin  32703  fundmfibi  32704  residfi  32707  uhgraopsiz  32783  diaf11N  37192  dibf11N  37304
  Copyright terms: Public domain W3C validator