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

Theorem funfn 5550
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 2452 . . 3  |-  dom  A  =  dom  A
21biantru 505 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5524 . 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 1370   dom cdm 4943   Fun wfun 5515    Fn wfn 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2444  df-fn 5524
This theorem is referenced by:  funssxp  5674  funforn  5730  funbrfvb  5838  funopfvb  5839  ssimaex  5860  fvco  5871  fvco4i  5873  eqfunfv  5906  fvimacnvi  5921  unpreima  5933  respreima  5936  elrnrexdm  5951  elrnrexdmb  5952  ffvresb  5978  funressn  5999  funresdfunsn  6024  resfunexg  6047  funex  6049  funiunfv  6069  elunirn  6072  suppval1  6801  funsssuppss  6820  smores  6918  smores2  6920  tfrlem1  6940  rdgsucg  6984  rdglimg  6986  mptfi  7716  ordtypelem4  7841  ordtypelem6  7843  ordtypelem7  7844  ordtypelem9  7846  ordtypelem10  7847  harwdom  7911  ackbij2  8518  brdom3  8801  brdom5  8802  brdom4  8803  smobeth  8856  fpwwe2lem11  8913  hashkf  12217  hashfun  12312  hashimarn  12313  fclim  13144  isstruct2  14296  xpsc0  14612  xpsc1  14613  invf  14820  coapm  15053  psgnghm  18130  lindfrn  18370  ofco2  18454  dfac14  19318  perfdvf  21506  c1lip2  21598  taylf  21954  usgra2edg  23448  usgrarnedg  23450  usgrafilem2  23472  cusgrares  23527  vdusgraval  23724  vdgrnn0pnf  23726  hlimf  24787  adj1o  25445  abrexdomjm  26035  iunpreima  26061  unipreima  26107  xppreima  26110  mptct  26164  mptctf  26167  sitgf  26872  orvcval2  26980  wfrlem4  27866  frrlem4  27910  elno3  27935  fullfunfnv  28116  fullfunfv  28117  abrexdom  28767  funcoressn  30176  funbrafvb  30205  funopafvb  30206  resfnfinfin  30308  vdn0frgrav2  30759  vdgn0frgrav2  30760  vdgfrgragt2  30763  diaf11N  35013  dibf11N  35125
  Copyright terms: Public domain W3C validator