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

Theorem funfn 6355
 Description: A class is a function if and only if it is a function on its domain. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn (Fun 𝐴𝐴 Fn dom 𝐴)

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2798 . . 3 dom 𝐴 = dom 𝐴
21biantru 533 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 6328 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 281 1 (Fun 𝐴𝐴 Fn dom 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  dom cdm 5520  Fun wfun 6319   Fn wfn 6320 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6328 This theorem is referenced by:  funfnd  6356  funssxp  6510  funforn  6573  funbrfvb  6696  funopfvb  6697  ssimaex  6724  fvco  6737  fvco4i  6740  eqfunfv  6785  fvimacnvi  6800  unpreima  6811  respreima  6814  elrnrexdm  6833  elrnrexdmb  6834  ffvresb  6866  funiun  6887  funressn  6899  funresdfunsn  6929  funex  6960  elunirn  6989  suppval1  7822  funsssuppss  7842  smores  7975  rdgsucg  8045  rdglimg  8047  fundmfibi  8790  residfi  8792  mptfi  8810  ordtypelem6  8974  ordtypelem7  8975  harwdom  9042  ackbij2  9657  mptct  9952  smobeth  10000  hashkf  13691  hashfun  13797  fclim  14905  coapm  17326  psgnghm  20274  lindfrn  20515  ausgrumgri  26970  dfnbgr3  27138  wlkiswwlks1  27663  vdn0conngrumgrv2  27991  hlimf  29030  adj1o  29687  abrexdomjm  30285  iunpreima  30338  fresf1o  30400  unipreima  30415  xppreima  30418  suppiniseg  30456  fdifsuppconst  30459  ressupprn  30460  mptctf  30489  orvcval2  31841  elno3  33290  noextenddif  33303  noextendlt  33304  noextendgt  33305  nosupbnd2lem1  33343  noetalem3  33347  fullfunfnv  33535  fullfunfv  33536  abrexdom  35187  diaf11N  38364  dibf11N  38476  gneispace3  40879  funbrafvb  43755  funopafvb  43756  funbrafv22b  43849  funopafv2b  43850
 Copyright terms: Public domain W3C validator