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

Theorem funfn 5833
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn (Fun 𝐴𝐴 Fn dom 𝐴)

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2610 . . 3 dom 𝐴 = dom 𝐴
21biantru 525 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 5807 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 266 1 (Fun 𝐴𝐴 Fn dom 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383   = wceq 1475  dom cdm 5038  Fun wfun 5798   Fn wfn 5799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807
This theorem is referenced by:  funssxp  5974  funforn  6035  funbrfvb  6148  funopfvb  6149  ssimaex  6173  fvco  6184  fvco4i  6186  eqfunfv  6224  fvimacnvi  6239  unpreima  6249  respreima  6252  elrnrexdm  6271  elrnrexdmb  6272  ffvresb  6301  funiun  6318  funressn  6331  funresdfunsn  6360  resfunexg  6384  funex  6387  funiunfv  6410  elunirn  6413  suppval1  7188  funsssuppss  7208  wfrlem4  7305  smores  7336  smores2  7338  tfrlem1  7359  rdgsucg  7406  rdglimg  7408  fundmfibi  8130  mptfi  8148  resfifsupp  8186  ordtypelem4  8309  ordtypelem6  8311  ordtypelem7  8312  ordtypelem9  8314  ordtypelem10  8315  harwdom  8378  ackbij2  8948  brdom3  9231  brdom5  9232  brdom4  9233  smobeth  9287  fpwwe2lem11  9341  hashkf  12981  hashfun  13084  hashimarn  13085  fclim  14132  isstruct2  15704  xpsc0  16043  xpsc1  16044  invf  16251  coapm  16544  psgnghm  19745  lindfrn  19979  ofco2  20076  dfac14  21231  perfdvf  23473  c1lip2  23565  taylf  23919  lpvtx  25734  upgrle2  25771  uhgrvtxedgiedgb  25810  usgra2edg  25911  usgrarnedg  25913  usgrafilem2  25941  cusgrares  26001  vdusgraval  26434  vdgrnn0pnf  26436  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdgfrgragt2  26554  hlimf  27478  adj1o  28137  abrexdomjm  28729  iunpreima  28765  fresf1o  28815  unipreima  28826  xppreima  28829  mptct  28880  mptctf  28883  sitgf  29736  orvcval2  29847  frrlem4  31027  elno3  31052  fullfunfnv  31223  fullfunfv  31224  abrexdom  32695  diaf11N  35356  dibf11N  35468  gneispace3  37451  gneispace  37452  gneispacef2  37454  funcoressn  39856  funbrafvb  39885  funopafvb  39886  resfnfinfin  40339  residfi  40340  resunimafz0  40368  ausgrumgri  40397  uhgr2edg  40435  ushgredgedga  40456  ushgredgedgaloop  40458  subgruhgredgd  40508  subuhgr  40510  subupgr  40511  subumgr  40512  subusgr  40513  dfnbgr3  40562  vtxdun  40696  upgrewlkle2  40808  1wlkiswwlks1  41064  vdn0conngrumgrv2  41363  eupthvdres  41403
  Copyright terms: Public domain W3C validator