Theorem funfn 6471

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 2739	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 530	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6440	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 277	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  dom cdm 5590  Fun wfun 6431   Fn wfn 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-fn 6440

This theorem is referenced by:  funfnd  6472  funssxp  6638  funforn  6704  funbrfvb  6833  funopfvb  6834  ssimaex  6862  fvco  6875  fvco4i  6878  eqfunfv  6923  fvimacnvi  6938  unpreima  6949  respreima  6952  elrnrexdm  6974  elrnrexdmb  6975  ffvresb  7007  funiun  7028  funressn  7040  funresdfunsn  7070  funex  7104  elunirn  7133  suppval1  7992  funsssuppss  8015  smores  8192  rdgsucg  8263  rdglimg  8265  imafi  8967  fundmfibi  9107  residfi  9109  mptfi  9127  ordtypelem6  9291  ordtypelem7  9292  harwdom  9359  ackbij2  10008  mptct  10303  smobeth  10351  hashkf  14055  hashfun  14161  fclim  15271  coapm  17795  psgnghm  20794  lindfrn  21037  ausgrumgri  27546  dfnbgr3  27714  wlkiswwlks1  28241  vdn0conngrumgrv2  28569  hlimf  29608  adj1o  30265  abrexdomjm  30861  iunpreima  30913  fresf1o  30975  unipreima  30990  xppreima  30992  suppiniseg  31029  fdifsuppconst  31032  ressupprn  31033  mptctf  31061  orvcval2  32434  fineqvac  33075  elno3  33867  noextenddif  33880  noextendlt  33881  noextendgt  33882  nosupbnd2lem1  33927  noetasuplem4  33948  fullfunfnv  34257  fullfunfv  34258  abrexdom  35897  diaf11N  39070  dibf11N  39182  gneispace3  41750  fresfo  44553  funbrafvb  44659  funopafvb  44660  funbrafv22b  44753  funopafv2b  44754