MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funfn Structured version   Visualization 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 2462 . . 3  |-  dom  A  =  dom  A
21biantru 512 . 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 260 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    = wceq 1455   dom cdm 4853   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 1680  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-cleq 2455  df-fn 5604
This theorem is referenced by:  funssxp  5765  funforn  5823  funbrfvb  5930  funopfvb  5931  ssimaex  5953  fvco  5964  fvco4i  5966  eqfunfv  6004  fvimacnvi  6019  unpreima  6029  respreima  6032  elrnrexdm  6049  elrnrexdmb  6050  ffvresb  6078  funressn  6101  funresdfunsn  6130  resfunexg  6155  funex  6158  funiunfv  6178  elunirn  6181  suppval1  6947  funsssuppss  6968  wfrlem4  7065  smores  7097  smores2  7099  tfrlem1  7120  rdgsucg  7167  rdglimg  7169  fundmfibi  7881  mptfi  7899  resfifsupp  7937  ordtypelem4  8062  ordtypelem6  8064  ordtypelem7  8065  ordtypelem9  8067  ordtypelem10  8068  harwdom  8131  ackbij2  8699  brdom3  8982  brdom5  8983  brdom4  8984  smobeth  9037  fpwwe2lem11  9091  hashkf  12549  hashfun  12642  hashimarn  12643  fclim  13666  isstruct2  15179  xpsc0  15515  xpsc1  15516  invf  15722  coapm  16015  psgnghm  19197  lindfrn  19428  ofco2  19525  dfac14  20682  perfdvf  22907  c1lip2  22999  taylf  23365  usgra2edg  25158  usgrarnedg  25160  usgrafilem2  25189  cusgrares  25249  vdusgraval  25684  vdgrnn0pnf  25686  vdn0frgrav2  25800  vdgn0frgrav2  25801  vdgfrgragt2  25804  hlimf  26939  adj1o  27596  abrexdomjm  28190  iunpreima  28229  fresf1o  28280  unipreima  28294  xppreima  28297  mptct  28351  mptctf  28354  sitgf  29229  orvcval2  29340  frrlem4  30566  elno3  30591  fullfunfnv  30762  fullfunfv  30763  abrexdom  32102  diaf11N  34662  dibf11N  34774  funcoressn  38666  funbrafvb  38696  funopafvb  38697  funiun  39059  resfnfinfin  39080  residfi  39081  lpvtx  39205  upgrle2  39241  uhgrvtxedgiedgb  39275  ausgrumgri  39302  uhgr2edg  39339  ushgredgedga  39356  ushgredgedgaloop  39358  subgruhgredgd  39406  subuhgr  39408  subupgr  39409  subumgr  39410  subusgr  39411  dfnbgr3  39458  vtxduhgrun  39588  upgrewlkle2  39673  uhgraopsiz  39977
  Copyright terms: Public domain W3C validator