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

Theorem funfn 5630
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 2429 . . 3  |-  dom  A  =  dom  A
21biantru 507 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5604 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 255 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    = wceq 1437   dom cdm 4854   Fun wfun 5595    Fn wfn 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421  df-fn 5604
This theorem is referenced by:  funssxp  5759  funforn  5817  funbrfvb  5923  funopfvb  5924  ssimaex  5946  fvco  5957  fvco4i  5959  eqfunfv  5996  fvimacnvi  6011  unpreima  6021  respreima  6024  elrnrexdm  6041  elrnrexdmb  6042  ffvresb  6069  funressn  6092  funresdfunsn  6121  resfunexg  6145  funex  6148  funiunfv  6168  elunirn  6171  suppval1  6931  funsssuppss  6952  wfrlem4  7047  smores  7079  smores2  7081  tfrlem1  7102  rdgsucg  7149  rdglimg  7151  fundmfibi  7861  mptfi  7879  resfifsupp  7917  ordtypelem4  8036  ordtypelem6  8038  ordtypelem7  8039  ordtypelem9  8041  ordtypelem10  8042  harwdom  8105  ackbij2  8671  brdom3  8954  brdom5  8955  brdom4  8956  smobeth  9009  fpwwe2lem11  9064  hashkf  12514  hashfun  12604  hashimarn  12605  fclim  13595  isstruct2  15093  xpsc0  15417  xpsc1  15418  invf  15624  coapm  15917  psgnghm  19079  lindfrn  19310  ofco2  19407  dfac14  20564  perfdvf  22735  c1lip2  22827  taylf  23181  usgra2edg  24955  usgrarnedg  24957  usgrafilem2  24985  cusgrares  25045  vdusgraval  25480  vdgrnn0pnf  25482  vdn0frgrav2  25596  vdgn0frgrav2  25597  vdgfrgragt2  25600  hlimf  26725  adj1o  27382  abrexdomjm  27977  iunpreima  28019  fresf1o  28071  unipreima  28085  xppreima  28088  mptct  28145  mptctf  28148  sitgf  29008  orvcval2  29117  frrlem4  30304  elno3  30329  fullfunfnv  30498  fullfunfv  30499  abrexdom  31761  diaf11N  34326  dibf11N  34438  funcoressn  38019  funbrafvb  38048  funopafvb  38049  resfnfinfin  38387  residfi  38388  uhgraopsiz  38462
  Copyright terms: Public domain W3C validator