Theorem funfn 6519

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 2737	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 531	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 6487	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 278	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1541  dom cdm 5625  Fun wfun 6478   Fn wfn 6479

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729  df-fn 6487

This theorem is referenced by:  funfnd  6520  funssxp  6685  funforn  6751  funbrfvb  6885  funopfvb  6886  ssimaex  6914  fvco  6927  fvco4i  6930  eqfunfv  6975  fvimacnvi  6990  unpreima  7001  respreima  7004  elrnrexdm  7026  elrnrexdmb  7027  ffvresb  7059  funiun  7080  funressn  7092  funresdfunsn  7122  funex  7156  elunirn  7185  suppval1  8058  funsssuppss  8081  smores  8258  rdgsucg  8329  rdglimg  8331  imafi  9045  fundmfibi  9201  residfi  9203  mptfi  9221  ordtypelem6  9385  ordtypelem7  9386  harwdom  9453  ackbij2  10105  mptct  10400  smobeth  10448  hashkf  14152  hashfun  14257  fclim  15362  coapm  17884  psgnghm  20891  lindfrn  21134  elno3  26909  noextenddif  26922  noextendlt  26923  noextendgt  26924  nosupbnd2lem1  26969  noetasuplem4  26990  ausgrumgri  27826  dfnbgr3  27994  wlkiswwlks1  28520  vdn0conngrumgrv2  28848  hlimf  29887  adj1o  30544  abrexdomjm  31139  iunpreima  31189  fresf1o  31251  unipreima  31266  xppreima  31268  suppiniseg  31305  fdifsuppconst  31308  ressupprn  31309  mptctf  31337  orvcval2  32723  fineqvac  33363  fullfunfnv  34385  fullfunfv  34386  abrexdom  36042  diaf11N  39366  dibf11N  39478  gneispace3  42114  fresfo  44958  funbrafvb  45064  funopafvb  45065  funbrafv22b  45158  funopafv2b  45159