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

Theorem funfn 5435
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 2433 . . 3  |-  dom  A  =  dom  A
21biantru 502 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5409 . 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 1362   dom cdm 4827   Fun wfun 5400    Fn wfn 5401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2426  df-fn 5409
This theorem is referenced by:  funssxp  5559  funforn  5615  funbrfvb  5722  funopfvb  5723  ssimaex  5744  fvco  5755  fvco4i  5757  eqfunfv  5790  fvimacnvi  5805  unpreima  5817  respreima  5820  elrnrexdm  5835  elrnrexdmb  5836  ffvresb  5861  funressn  5882  funresdfunsn  5907  resfunexg  5930  funex  5932  funiunfv  5952  elunirnALT  5957  suppval1  6685  funsssuppss  6704  smores  6799  smores2  6801  tfrlem1  6821  rdgsucg  6865  rdglimg  6867  mptfi  7598  ordtypelem4  7723  ordtypelem6  7725  ordtypelem7  7726  ordtypelem9  7728  ordtypelem10  7729  harwdom  7793  ackbij2  8400  brdom3  8683  brdom5  8684  brdom4  8685  smobeth  8738  fpwwe2lem11  8794  hashkf  12088  hashfun  12182  hashimarn  12183  fclim  13014  isstruct2  14165  xpsc0  14480  xpsc1  14481  invf  14688  coapm  14921  psgnghm  17851  lindfrn  18091  ofco2  18173  dfac14  19032  perfdvf  21219  c1lip2  21311  taylf  21710  usgra2edg  23123  usgrarnedg  23125  usgrafilem2  23147  cusgrares  23202  vdusgraval  23399  vdgrnn0pnf  23401  hlimf  24462  adj1o  25120  abrexdomjm  25711  iunpreima  25738  unipreima  25784  xppreima  25787  mptct  25841  mptctf  25844  sitgf  26580  orvcval2  26688  wfrlem4  27573  frrlem4  27617  elno3  27642  fullfunfnv  27823  fullfunfv  27824  abrexdom  28465  funcoressn  29876  funbrafvb  29905  funopafvb  29906  resfnfinfin  30008  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdgfrgragt2  30463  diaf11N  34264  dibf11N  34376
  Copyright terms: Public domain W3C validator