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

Theorem funfn 5283
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 2283 . . 3  |-  dom  A  =  dom  A
21biantru 491 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5258 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 243 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1623   dom cdm 4689   Fun wfun 5249    Fn wfn 5250
This theorem is referenced by:  funssxp  5402  funforn  5458  funbrfvb  5565  funopfvb  5566  ssimaex  5584  fvco  5595  fvco4i  5597  eqfunfv  5627  fvimacnvi  5639  unpreima  5651  respreima  5654  ffvresb  5690  funressn  5706  resfunexg  5737  funex  5743  funiunfv  5774  elunirnALT  5779  smores  6369  smores2  6371  rdgsucg  6436  rdglimg  6438  mptfi  7155  ordtypelem4  7236  ordtypelem6  7238  ordtypelem7  7239  ordtypelem9  7241  ordtypelem10  7242  harwdom  7304  ackbij2  7869  brdom3  8153  brdom5  8154  brdom4  8155  smobeth  8208  fpwwe2lem11  8262  hashkf  11339  hashfun  11389  fclim  12027  isstruct2  13157  xpsc0  13462  xpsc1  13463  invf  13670  coapm  13903  dfac14  17312  perfdvf  19253  c1lip2  19345  taylf  19740  hlimf  21817  adj1o  22474  abrexdomjm  23165  unipreima  23209  xppreima  23211  mptct  23345  mptctf  23348  orvcval2  23659  wfrlem4  24259  frrlem4  24284  elno3  24309  fullfunfnv  24484  fullfunfv  24485  abrexdom  26405  lindfrn  27291  psgnghm  27437  funcoressn  27990  funbrafvb  28018  funopafvb  28019  diaf11N  31239  dibf11N  31351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258
  Copyright terms: Public domain W3C validator