Theorem funfn 6584

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

Step	Hyp	Ref	Expression
1		eqid 2725	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 528	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6552	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 277	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533  dom cdm 5678  Fun wfun 6543   Fn wfn 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-fn 6552

This theorem is referenced by:  funfnd  6585  funssxp  6752  funforn  6817  funbrfvb  6951  funopfvb  6952  ssimaex  6982  fvco  6995  fvco4i  6998  eqfunfv  7044  fvimacnvi  7060  unpreima  7071  respreima  7074  elrnrexdm  7098  elrnrexdmb  7099  ffvresb  7134  funiun  7156  funressn  7168  funresdfunsn  7198  funex  7231  elunirn  7261  suppval1  8171  funsssuppss  8195  smores  8373  rdgsucg  8444  rdglimg  8446  imafi  9200  fundmfibi  9357  residfi  9359  mptfi  9377  ordtypelem6  9548  ordtypelem7  9549  harwdom  9616  ackbij2  10268  mptct  10563  smobeth  10611  hashkf  14327  hashfun  14432  fclim  15533  coapm  18063  psgnghm  21529  lindfrn  21772  elno3  27634  noextenddif  27647  noextendlt  27648  noextendgt  27649  nosupbnd2lem1  27694  noetasuplem4  27715  ausgrumgri  29052  dfnbgr3  29223  wlkiswwlks1  29750  vdn0conngrumgrv2  30078  hlimf  31119  adj1o  31776  abrexdomjm  32380  iunpreima  32434  fresf1o  32497  unipreima  32511  xppreima  32513  suppiniseg  32548  fdifsuppconst  32551  ressupprn  32552  mptctf  32581  orvcval2  34209  fineqvac  34848  fullfunfnv  35673  fullfunfv  35674  abrexdom  37334  diaf11N  40652  dibf11N  40764  imadomfi  41605  gneispace3  43705  fresfo  46568  funbrafvb  46674  funopafvb  46675  funbrafv22b  46768  funopafv2b  46769  dfclnbgr3  47302  grimuhgr  47362